Go to the documentation of this file.
33 std::set<symbol_exprt> symbols;
35 for(
const auto &i : goto_function.body.instructions)
40 if(i_it==goto_function.body.instructions.begin())
48 if(previous->is_goto() && !previous->get_condition().is_true())
52 else if(previous->is_function_call() && !previous->guard.is_true())
56 else if(i_it->is_target() || i_it->is_function_call())
68 for(
const auto &symbol_expr : symbols)
72 assertion.push_back(tmp);
75 if(!assertion.empty())
78 goto_function.body.insert_before_swap(i_it);
81 t->source_location=i_it->source_location;
#define Forall_goto_program_instructions(it, program)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Base class for all expressions.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
bool is_true() const
Return whether the expression is a constant representing true.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void instrument_intervals(const ait< interval_domaint > &interval_analysis, goto_functionst::goto_functiont &goto_function)
Instruments all "post-branch" instructions with assumptions about variable intervals.
std::vector< exprt > operandst
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
#define Forall_goto_functions(it, functions)
::goto_functiont goto_functiont
goto_functionst goto_functions
GOTO functions.
exprt make_expression(const symbol_exprt &) const
instructionst::const_iterator const_targett
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
symbol_tablet symbol_table
Symbol table.
instructionst::iterator targett
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...