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());
132 for(
const auto &expr : lhs_syms)
133 if(curr.find(expr)!=curr.end())
139 next.erase(assignment.
lhs());
150 if(expr.
id() == ID_symbol ||
151 expr.
id() == ID_index ||
152 expr.
id() == ID_member ||
153 expr.
id() == ID_dereference)