28 bool _assume_non_null,
39 const typet &expected_type,
44 unsigned insert_before_index,
46 bool update_in_place);
78 const typet &expected_type,
83 const unsigned insert_before_index,
85 const bool update_in_place)
92 expected_type.
id() == ID_pointer,
93 "Nondet initializer result type: expected a pointer",
98 const auto &expected_base = ns.follow(expected_type.
subtype());
99 if(expected_base.id() != ID_struct)
102 const exprt cast_ptr =
105 exprt to_init = cast_ptr;
130 if(!new_instructions.
operands().empty())
132 auto insert_position = parent_block.
operands().begin();
133 std::advance(insert_position, insert_before_index);
136 new_instructions.
operands().begin(),
160 const auto &this_argument = required_type.
parameters()[0];
161 const typet &this_type = this_argument.type();
166 synthesized_source_location,
171 init_symbol_expression,
symbol_exprt(this_argument.get_identifier()));
176 init_symbol_expression,
177 synthesized_source_location,
190 required_return_type,
193 synthesized_source_location,
197 if(to_return_symbol.
type.
id() != ID_pointer)
215 required_return_type,
217 synthesized_source_location,
227 symbol.
value = new_instructions;
239 sym.
name !=
"java::monitorenter" && sym.
name !=
"java::monitorexit")
248 bool assume_non_null,
253 symbol_table, assume_non_null, object_factory_parameters,
message_handler);
269 bool assume_non_null,
279 std::vector<irep_idt> identifiers;
280 identifiers.reserve(symbol_table.
symbols.size());
281 for(
const auto &symbol : symbol_table)
282 identifiers.push_back(symbol.first);
285 symbol_table, assume_non_null, object_factory_parameters,
message_handler);
287 for(
const auto &identifier : identifiers)
The type of an expression.
irep_idt name
The unique identifier.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
void set_function(const irep_idt &function)
void create_method_stub(symbolt &symbol)
Replaces sym's value with an opaque method stub.
static bool is_constructor(const irep_idt &method_name)
const std::string & id2string(const irep_idt &d)
java_simple_method_stubst(symbol_table_baset &_symbol_table, bool _assume_non_null, const object_factory_parameterst &_object_factory_parameters, message_handlert &_message_handler)
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void copy_to_operands(const exprt &expr)
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
Fresh auxiliary symbol creation.
Allocate local stacked objects.
Java simple opaque stub generation.
exprt value
Initial value of symbol.
void create_method_stub_at(const typet &expected_type, const exprt &ptr, const source_locationt &loc, const irep_idt &function_id, code_blockt &parent_block, unsigned insert_before_index, bool is_constructor, bool update_in_place)
Nondet-initialize an object, including allocating referees for reference fields and nondet-initialisi...
void java_generate_simple_method_stub(const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_is_constructor() const
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Operator to dereference a pointer.
API to expression classes.
message_handlert & message_handler
const object_factory_parameterst & object_factory_parameters
typet type
Type of symbol.
Allocate dynamic objects (using MALLOC)
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Base class for all expressions.
const parameterst & parameters() const
The symbol table base class interface.
void java_generate_simple_method_stubs(symbol_table_baset &symbol_table, bool assume_non_null, const object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
Generates function stubs for most undefined functions in the symbol table, except as forbidden in jav...
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...
symbol_table_baset & symbol_table
source_locationt & add_source_location()
Expression to hold a symbol (variable)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
goto_programt coverage_criteriont message_handlert & message_handler
const typet & subtype() const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & return_type() const
void check_method_stub(const irep_idt &)
Replaces sym with a function stub per the function above if it is of suitable type.
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)
size_t max_nonnull_tree_depth
To force a certain depth of non-null objects.