28 bool _assume_non_null,
39 const typet &expected_type,
44 unsigned insert_before_index,
46 bool update_in_place);
80 const typet &expected_type,
85 const unsigned insert_before_index,
87 const bool update_in_place)
94 expected_type.
id() == ID_pointer,
95 "Nondet initializer result type: expected a pointer",
100 const auto &expected_base = ns.follow(expected_type.
subtype());
101 if(expected_base.id() != ID_struct)
104 const exprt cast_ptr =
107 exprt to_init = cast_ptr;
134 auto insert_position = parent_block.
statements().begin();
135 std::advance(insert_position, insert_before_index);
162 const auto &this_argument = required_type.
parameters()[0];
163 const typet &this_type = this_argument.type();
168 synthesized_source_location,
173 init_symbol_expression,
symbol_exprt(this_argument.get_identifier()));
175 new_instructions.
add(get_argument);
178 init_symbol_expression,
179 synthesized_source_location,
192 required_return_type,
195 synthesized_source_location,
199 if(to_return_symbol.
type.
id() != ID_pointer)
217 required_return_type,
219 synthesized_source_location,
229 symbol.
value = new_instructions;
239 sym.
type.
id() == ID_code &&
246 "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" &&
248 "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V")
257 bool assume_non_null,
262 symbol_table, assume_non_null, object_factory_parameters, message_handler);
278 bool assume_non_null,
288 std::vector<irep_idt> identifiers;
289 identifiers.reserve(symbol_table.
symbols.size());
290 for(
const auto &symbol : symbol_table)
291 identifiers.push_back(symbol.first);
294 symbol_table, assume_non_null, object_factory_parameters, message_handler);
296 for(
const auto &identifier : identifiers)
The type of an expression, extends irept.
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)
void java_generate_simple_method_stubs(symbol_table_baset &symbol_table, bool assume_non_null, const java_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...
const std::string & id2string(const irep_idt &d)
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
code_operandst & statements()
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...
java_simple_method_stubst(symbol_table_baset &_symbol_table, bool _assume_non_null, const java_object_factory_parameterst &_object_factory_parameters, message_handlert &_message_handler)
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
void add(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Operator to dereference a pointer.
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const java_object_factory_parameterst & object_factory_parameters
message_handlert & message_handler
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
typet type
Type of symbol.
Allocate dynamic objects (using MALLOC)
const java_method_typet & to_java_method_type(const typet &type)
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.
symbol_table_baset & symbol_table
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...
source_locationt & add_source_location()
A codet representing sequential composition of program statements.
Expression to hold a symbol (variable)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
codet representation of a "return from a function" statement.
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 java_generate_simple_method_stub(const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const java_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
A codet representing an assignment in the program.
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)