33 const bool non_void_non_function_pointer = type.
id() == ID_pointer &&
37 non_void_non_function_pointer;
51 const bool skip_classid =
true;
59 object_factory_parameters,
64 gen_nondet_init_code, symbol_table, instructions, message_handler, mode);
88 const auto next_instr = std::next(target);
102 if(!nondet_expr.get_nullable())
125 const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
126 op = aux_symbol_expr;
144 object_factory_parameters,
149 dead_aux_symbol->make_dead();
150 dead_aux_symbol->code =
code_deadt(aux_symbol_expr);
151 dead_aux_symbol->source_location = source_loc;
156 return std::make_pair(target2,
true);
159 return std::make_pair(next_instr,
false);
178 bool changed =
false;
179 auto instruction_iterator = goto_program.
instructions.begin();
181 while(instruction_iterator != goto_program.
instructions.end())
185 instruction_iterator,
188 object_factory_parameters,
190 instruction_iterator = ret.first;
191 changed |= ret.second;
207 parameters.
function_id =
function.get_function_id();
209 function.get_goto_function().body,
210 function.get_symbol_table(),
215 function.compute_location_numbers();
230 if(symbol.
mode==ID_java)
238 object_factory_parameters,
257 object_factory_parameters);
The type of an expression, extends irept.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
void update()
Update all indices.
void convert_nondet(goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_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...
const std::string & id2string(const irep_idt &d)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
irep_idt mode
Language mode.
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
typet & type()
Return the type of the expression.
symbol_tablet symbol_table
Symbol table.
This class represents an instruction in the GOTO intermediate representation.
static std::pair< goto_programt::targett, bool > insert_nondet_init_code(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.
const irep_idt & id() const
void compute_location_numbers()
instructionst::iterator targett
A codet representing the declaration of a local variable.
instructionst instructions
The list of instructions in the goto program.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Convert side_effect_expr_nondett expressions using java_object_factory.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
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...
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
A collection of goto functions.
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.
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
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
A generic container class for the GOTO intermediate representation of one function.
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.
source_locationt source_location
The location of the instruction in the source file.
Base class for all expressions.
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
A codet representing the removal of a local variable going out of scope.
static const irep_idt get_function_id(const_targett l)
Get the id of the function that contains the instruction pointed-to by the given instruction iterator...
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...
A codet representing sequential composition of program statements.
Expression to hold a symbol (variable)
const typet & subtype() const
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Interface providing access to a single function in a GOTO model, plus its associated symbol table...