43 const auto next_instr=std::next(target);
44 if(!target->is_assign())
51 if(assign.rhs().id()!=ID_side_effect)
58 if(side_effect.get_statement()!=ID_nondet)
63 const auto lhs=assign.lhs();
66 if(!lhs.type().has_subtype())
72 if(lhs.type().subtype().id()==ID_empty ||
73 lhs.type().subtype().id()==ID_code)
82 const auto source_loc=target->source_location;
96 object_factory_parameters,
127 instruction_iterator!=end;)
131 instruction_iterator,
134 object_factory_parameters,
146 parameters.
function_id =
function.get_function_id();
148 function.get_goto_function().body,
149 function.get_symbol_table(),
154 function.compute_location_numbers();
169 if(symbol.
mode==ID_java)
177 object_factory_parameters,
196 object_factory_parameters);
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
void update()
Update all indices.
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
irep_idt mode
Language mode.
bool get_nullable() const
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Fresh auxiliary symbol creation.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_assignt & to_code_assign(const codet &code)
void compute_location_numbers()
instructionst::iterator targett
static goto_programt::targett insert_nondet_init_code(goto_programt &goto_program, const goto_programt::targett &target, symbol_table_baset &symbol_table, message_handlert &message_handler, 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.
instructionst instructions
The list of instructions in the goto program.
Convert side_effect_expr_nondett expressions.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
A generic container class for the GOTO intermediate representation of one function.
Allocate dynamic objects (using MALLOC)
void convert_nondet(goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const object_factory_parameterst &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...
The symbol table base class interface.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
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...
goto_programt & goto_program
goto_programt coverage_criteriont message_handlert & message_handler
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
size_t max_nonnull_tree_depth
To force a certain depth of non-null objects.
Interface providing access to a single function in a GOTO model, plus its associated symbol table...