28 switch(from_l->type())
34 exprt tmp(from_l->condition());
36 if(std::next(from_l) == to_l)
47 exprt tmp(from_l->condition());
58 invariant_set.assignment(from_l->assign_lhs(), from_l->assign_rhs());
62 if(from_l->get_other().is_not_nil())
80 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
92 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
virtual const locationt & current_location(void) const =0
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
invariant_sett invariant_set
virtual void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...