24 for(goto_programt::instructionst::const_reverse_iterator
46 std::cout <<
"Previous cone: \n";
48 for(
const auto &expr :
curr)
49 std::cout <<
expr2c(expr,
ns) <<
" ";
51 std::cout <<
"\nCurrent cone: \n";
53 for(
const auto &expr : next)
54 std::cout <<
expr2c(expr,
ns) <<
" ";
73 goto_programt::instructionst::const_reverse_iterator
rit,
81 goto_programt::instructionst::const_reverse_iterator next=
rit;
86 if(!
rit->get_condition().is_false())
89 for(goto_programt::targetst::const_iterator t=
rit->targets.begin();
90 t !=
rit->targets.end();
93 unsigned int loc=(*t)->location_number;
95 targets.insert(s.begin(), s.end());
99 if(
rit->get_condition().is_true())
104 else if(
rit->is_assume() ||
rit->is_assert())
106 if(
rit->get_condition().is_false())
112 unsigned int loc=next->location_number;
114 targets.insert(s.begin(), s.end());
122 next.insert(
curr.begin(),
curr.end());
138 next.erase(
i.assign_lhs());
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const goto_programt & program
void get_succs(goto_programt::instructionst::const_reverse_iterator rit, expr_sett &targets)
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
void gather_rvalues(const exprt &expr, expr_sett &rvals)
Base class for all expressions.
This class represents an instruction in the GOTO intermediate representation.
instructionst instructions
The list of instructions in the goto program.
const irep_idt & id() const
std::unordered_set< exprt, irep_hash > expr_sett
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
#define forall_operands(it, expr)