Loading...

Searching...

No Matches

object_creation_referencet Struct Reference

Information to store when several references point to the same Java object. More...

+ Collaboration diagram for object_creation_referencet:

Public Attributes

Expression for the symbol that stores the value that may be reference equal to other values.

std::optional< exprt > array_length

If symbol is an array, this expression stores its length.

Detailed Description

Information to store when several references point to the same Java object.

Definition at line 23 of file code_with_references.h.

std::optional<exprt> object_creation_referencet::array_length

If symbol is an array, this expression stores its length.

This should only be set once the actual elements of the array have been seen, not the first time an @ref have been seen, only when @id is seen.

Definition at line 33 of file code_with_references.h.

exprt object_creation_referencet::expr

Expression for the symbol that stores the value that may be reference equal to other values.

Definition at line 27 of file code_with_references.h.

The documentation for this struct was generated from the following file: