22 std::set<symbol_exprt> symbols;
32 if(i_it==goto_function.body.instructions.begin())
40 if(previous->is_goto() && !previous->guard.is_true())
44 else if(previous->is_function_call() && !previous->guard.is_true())
48 else if(i_it->is_target() || i_it->is_function_call())
60 for(
const auto &symbol_expr : symbols)
64 assertion.push_back(tmp);
67 if(!assertion.empty())
70 goto_function.body.insert_before_swap(i_it);
73 t->source_location=i_it->source_location;
74 t->function=i_it->function;
exprt conjunction(const exprt::operandst &op)
instructionst::const_iterator const_targett
goto_function_templatet< goto_programt > goto_functiont
exprt make_expression(const symbol_exprt &) const
std::vector< exprt > operandst
void instrument_intervals(const ait< interval_domaint > &interval_analysis, goto_functionst::goto_functiont &goto_function)
Base class for all expressions.
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
#define forall_goto_program_instructions(it, program)
void find_symbols(const exprt &src, find_symbols_sett &dest)
void interval_analysis(const namespacet &ns, goto_functionst &goto_functions)
instructionst::iterator targett