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
166 size_t max_nondet_array_length);
168 #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.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
The type of an expression, extends irept.
Base class for all expressions.
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
code_blockt gen_nondet_array_init(const exprt &expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_tablet &symbol_table, size_t max_nondet_array_length)
Synthesize GOTO for generating a array of nondet length to be stored in the expr.
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, lifetimet lifetime, const source_locationt &location, const select_pointer_typet &pointer_type_selector, message_handlert &log)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
The symbol table base class interface.
lifetimet
Selects the kind of objects allocated.
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
std::function< code_blockt(const exprt &element_at_counter, const typet &element_type)> array_element_generatort