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;
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.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
void update()
Update all indices.
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
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...
This class represents an instruction in the GOTO intermediate representation.
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 object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
Populate instructions with goto instructions to nondet init aux_symbol_expr
const irep_idt & id() const
void compute_location_numbers()
instructionst::iterator targett
A declaration of a local variable.
instructionst instructions
The list of instructions in the goto program.
Convert side_effect_expr_nondett expressions.
targett insert_after(const_targett target)
Insertion after the given 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 at the given location.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
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...
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
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...
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, 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.
A removal of a local variable.
static const irep_idt get_function_id(const_targett l)
goto_programt & goto_program
Expression to hold a symbol (variable)
goto_programt coverage_criteriont message_handlert & message_handler
const typet & subtype() const
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...