58 object_factory_parameters,
95 for(
exprt &op : target->code_nonconst().operands())
120 op.type(),
"nondet_tmp",
source_loc, function_identifier, symbol_table);
140 object_factory_parameters,
150 return std::make_pair(
target2,
true);
167 const irep_idt &function_identifier,
176 object_factory_parameters.
function_id = function_identifier;
178 bool changed =
false;
189 object_factory_parameters,
192 changed |=
ret.second;
212 object_factory_parameters,
237 object_factory_parameters,
256 object_factory_parameters);
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A codet representing sequential composition of program statements.
A goto_instruction_codet representing the declaration of a local variable.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
void compute_location_numbers()
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
const irep_idt & get_function_id()
Get function id.
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
void compute_location_numbers()
Re-number our goto_function.
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void update()
Update all indices.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
The symbol table base class interface.
irep_idt mode
Language mode.
The type of an expression, extends irept.
static bool is_nondet_pointer(exprt expr)
Returns true if expr is a nondet pointer that isn't a function pointer or a void* pointer as these ca...
static std::pair< goto_programt::targett, bool > insert_nondet_init_code(const irep_idt &function_identifier, goto_programt &goto_program, const goto_programt::targett &target, symbol_table_baset &symbol_table, message_handlert &message_handler, java_object_factory_parameterst object_factory_parameters, const irep_idt &mode)
Checks an instruction to see whether it contains an assignment from side_effect_expr_nondet.
static goto_programt get_gen_nondet_init_instructions(const symbol_exprt &aux_symbol_expr, const source_locationt &source_loc, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
Populate instructions with goto instructions to nondet init aux_symbol_expr
void convert_nondet(const irep_idt &function_identifier, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &user_object_factory_parameters, const irep_idt &mode)
For each instruction in the goto program, checks if it is an assignment from nondet and replaces it w...
Convert side_effect_expr_nondett expressions using java_object_factory.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
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...
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
size_t min_null_tree_depth
To force a certain depth of non-null objects.