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,
155 const std::size_t &max_nondet_string_length,
161 #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.
codet initialize_nondet_string_struct(const exprt &obj, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable)
Initialize a nondeterministic String structure.
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...
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.
A statement in a programming language.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...