Values passed around between most functions of the recursive deterministic assignment algorithm entered from assign_from_json. More...
Collaboration diagram for object_creation_infot:Public Attributes | |
| allocate_objectst & | allocate_objects |
Handles allocation of new symbols, adds them to its symbol table (which will usually be the same as the symbol_table of this struct) and keeps track of them so declarations for them can be added by the caller before block. More... | |
| symbol_table_baset & | symbol_table |
| Used for looking up symbols corresponding to Java classes and methods. More... | |
| optionalt< ci_lazy_methods_neededt > & | needed_lazy_methods |
| Where runtime types differ from compile-time types, we need to mark the runtime types as needed by lazy methods. More... | |
| std::unordered_map< std::string, object_creation_referencet > & | references |
| Map to keep track of reference-equal objects. More... | |
| const source_locationt & | loc |
| Source location associated with the newly added codet. More... | |
| size_t | max_user_array_length |
| Maximum value allowed for any (constant or variable length) arrays in user code. More... | |
| const java_class_typet & | declaring_class_type |
| Used for the workaround for enums only. More... | |
Detailed Description
Values passed around between most functions of the recursive deterministic assignment algorithm entered from assign_from_json.
The values in a given object_creation_infot are never reassigned, but the ones that are not marked const may be mutated.
Definition at line 34 of file assignments_from_json.cpp.
Member Data Documentation
◆ allocate_objects
| allocate_objectst& object_creation_infot::allocate_objects |
Handles allocation of new symbols, adds them to its symbol table (which will usually be the same as the symbol_table of this struct) and keeps track of them so declarations for them can be added by the caller before block.
Definition at line 40 of file assignments_from_json.cpp.
◆ declaring_class_type
| const java_class_typet& object_creation_infot::declaring_class_type |
Used for the workaround for enums only.
See assign_enum_from_json.
Definition at line 63 of file assignments_from_json.cpp.
◆ loc
| const source_locationt& object_creation_infot::loc |
Source location associated with the newly added codet.
Definition at line 55 of file assignments_from_json.cpp.
◆ max_user_array_length
| size_t object_creation_infot::max_user_array_length |
Maximum value allowed for any (constant or variable length) arrays in user code.
Definition at line 59 of file assignments_from_json.cpp.
◆ needed_lazy_methods
| optionalt<ci_lazy_methods_neededt>& object_creation_infot::needed_lazy_methods |
Where runtime types differ from compile-time types, we need to mark the runtime types as needed by lazy methods.
Definition at line 47 of file assignments_from_json.cpp.
◆ references
| std::unordered_map<std::string, object_creation_referencet>& object_creation_infot::references |
Map to keep track of reference-equal objects.
Each entry has an ID (such that any two reference-equal objects have the same ID) and the expression for the symbol that all these references point to.
Definition at line 52 of file assignments_from_json.cpp.
◆ symbol_table
| symbol_table_baset& object_creation_infot::symbol_table |
Used for looking up symbols corresponding to Java classes and methods.
Definition at line 43 of file assignments_from_json.cpp.
The documentation for this struct was generated from the following file:
- /home/runner/work/cbmc-documentation/cbmc-documentation/jbmc/src/java_bytecode/assignments_from_json.cpp
