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);
74 t->function=i_it->function;
symbol_tablet symbol_table
Symbol table.
exprt conjunction(const exprt::operandst &op)
instructionst::iterator targett
instructionst::const_iterator const_targett
::goto_functiont 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)
const source_locationt & source_location() const
#define Forall_goto_program_instructions(it, program)
void interval_analysis(goto_modelt &goto_model)
#define forall_goto_program_instructions(it, program)
void find_symbols(const exprt &src, find_symbols_sett &dest)
goto_functionst goto_functions
GOTO functions.