28 for(goto_programt::instructionst::const_reverse_iterator
50 std::cout <<
"Previous cone: \n";
52 for(
const auto &expr : curr)
53 std::cout <<
expr2c(expr,
ns) <<
" ";
55 std::cout <<
"\nCurrent cone: \n";
57 for(
const auto &expr : next)
58 std::cout <<
expr2c(expr,
ns) <<
" ";
77 goto_programt::instructionst::const_reverse_iterator rit,
85 goto_programt::instructionst::const_reverse_iterator next=rit;
90 if(!rit->get_condition().is_false())
93 for(goto_programt::targetst::const_iterator t=rit->targets.begin();
94 t != rit->targets.end();
97 unsigned int loc=(*t)->location_number;
99 targets.insert(s.begin(), s.end());
103 if(rit->get_condition().is_true())
108 else if(rit->is_assume() || rit->is_assert())
110 if(rit->get_condition().is_false())
116 unsigned int loc=next->location_number;
118 targets.insert(s.begin(), s.end());
126 next.insert(curr.begin(), curr.end());
136 for(
const auto &expr : lhs_syms)
137 if(curr.find(expr)!=curr.end())
143 next.erase(assignment.
lhs());
154 if(expr.
id() == ID_symbol ||
155 expr.
id() == ID_index ||
156 expr.
id() == ID_member ||
157 expr.
id() == ID_dereference)
A codet representing an assignment in the program.
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.
codet code
Do not read or modify directly – use get_X() instead.
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)
const code_assignt & to_code_assign(const codet &code)