68 assert(!loop.empty());
71 std::map<unsigned, goto_programt::targett> loop_map;
73 for(loopt::const_iterator l_it=loop.begin();
76 loop_map[(*l_it)->location_number]=*l_it;
89 for(modifiest::const_iterator
90 m_it=modifies.begin();
99 t->function=loop_head->function;
100 t->source_location=loop_head->source_location;
102 t->code.add_source_location()=loop_head->source_location;
110 assert(!loop.empty());
129 for(loopt::const_iterator
130 l_it=loop.begin(); l_it!=loop.end(); l_it++)
135 for(goto_programt::targetst::iterator
136 t_it=instruction.
targets.begin();
137 t_it!=instruction.
targets.end();
154 for(loopt::const_iterator
155 i_it=loop.begin(); i_it!=loop.end(); i_it++)
168 const exprt &lhs=code_function_call.
lhs();
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void get_modifies(const loopt &, modifiest &)
bool is_function_call() const
std::set< goto_programt::targett > natural_loopt
typet & type()
Return the type of the expression.
targetst targets
The list of successor instructions.
This class represents an instruction in the GOTO intermediate representation.
const code_assignt & to_code_assign(const codet &code)
havoc_loopst(function_modifiest &_function_modifies, goto_functiont &_goto_function)
local_may_aliast local_may_alias
instructionst::iterator targett
void get_modifies_lhs(const local_may_aliast &, const goto_programt::const_targett, const exprt &lhs, modifiest &)
API to expression classes.
std::set< exprt > modifiest
::goto_functiont goto_functiont
A side_effect_exprt that returns a non-deterministically chosen value.
codet representation of a function call statement.
natural_loops_mutablet natural_loops
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
const natural_loops_mutablet::natural_loopt loopt
void havoc_loops(goto_modelt &goto_model)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
goto_functionst::goto_functiont goto_functiont
goto_functiont & goto_function
#define Forall_goto_functions(it, functions)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
void havoc_loop(const goto_programt::targett loop_head, const loopt &)
function_modifiest & function_modifies
Compute natural loops in a goto_function.
goto_programt::targett get_loop_exit(const loopt &)
goto_functionst goto_functions
GOTO functions.
A codet representing an assignment in the program.
Field-insensitive, location-sensitive may-alias analysis.
const code_function_callt & to_code_function_call(const codet &code)