68 #ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H 69 #define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H 137 const exprt &target_expr,
138 const typet &allocate_type,
143 std::vector<const symbolt *> &symbols_created,
144 bool cast_needed =
false);
147 const exprt &target_expr,
153 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
The type of an expression.
allocation_typet
Selects the kind of allocation used by java_object_factory et al.
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.
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, 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...
Allocate local stacked objects.
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 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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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.
Allocate dynamic objects (using MALLOC)
Base class for all expressions.
The symbol table base class interface.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...