Go to the documentation of this file.
71 #ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
72 #define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
140 const exprt &target_expr,
141 const typet &allocate_type,
146 std::vector<const symbolt *> &symbols_created,
147 bool cast_needed =
false);
150 const exprt &target_expr,
156 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, allocation_typet alloc_type, const source_locationt &location, const select_pointer_typet &pointer_type_selector)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
exprt allocate_dynamic_object_with_decl(const exprt &target_expr, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code)
Generates code for allocating a dynamic object.
@ GLOBAL
Allocate global objects.
The type of an expression, extends irept.
@ LOCAL
Allocate local stacked objects.
Base class for all expressions.
The symbol table base class interface.
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
exprt allocate_dynamic_object(const exprt &target_expr, const typet &allocate_type, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code, std::vector< const symbolt * > &symbols_created, bool cast_needed=false)
Generates code for allocating a dynamic object.
allocation_typet
Selects the kind of allocation used by java_object_factory et al.
@ DYNAMIC
Allocate dynamic objects (using MALLOC)