Loading...

Searching...

No Matches

object_creation_infot Struct Reference

Values passed around between most functions of the recursive deterministic assignment algorithm entered from assign_from_json. More...

+ Collaboration diagram for object_creation_infot:

[フレーム]

[legend]

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.

symbol_table_baset & symbol_table

Used for looking up symbols corresponding to Java classes and methods.

std::optional< 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.

std::unordered_map< std::string, object_creation_referencet > & references

Map to keep track of reference-equal objects.

const source_locationt & loc

Source location associated with the newly added codet.

size_t max_user_array_length

Maximum value allowed for any (constant or variable length) arrays in user code.

const java_class_typet & declaring_class_type

Used for the workaround for enums only.

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 35 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 41 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 64 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 56 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 60 of file assignments_from_json.cpp.

◆ needed_lazy_methods

std::optional<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 48 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 53 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 44 of file assignments_from_json.cpp.

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

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/assignments_from_json.cpp