object_creation_referencet Struct Reference
Information to store when several references point to the same Java object. More...
#include <code_with_references.h>
Collaboration diagram for object_creation_referencet:Public Attributes | |
| exprt | expr |
| Expression for the symbol that stores the value that may be reference equal to other values. More... | |
| std::optional< exprt > | array_length |
If symbol is an array, this expression stores its length. More... | |
Detailed Description
Information to store when several references point to the same Java object.
Definition at line 23 of file code_with_references.h.
Member Data Documentation
◆ array_length
| 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.
◆ expr
| 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:
- /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/code_with_references.h
