32 if(!step.guard_literal.is_constant())
34 if(step.is_assert() &&
35 !step.cond_literal.is_constant())
42 for(symex_target_equationt::SSA_stepst::const_iterator
46 if(it->is_assignment() &&
50 if(!it->guard_literal.is_constant())
52 lpoints[it->guard_literal].target=it->source.pc;
53 lpoints[it->guard_literal].score=0;
63 symex_target_equationt::SSA_stepst::const_iterator
66 for(symex_target_equationt::SSA_stepst::const_iterator
81 assert(value.size()==lpoints.size());
83 lpoints_valuet::const_iterator v_it=value.begin();
84 for(
const auto &l : lpoints)
87 assumptions.push_back(l.first);
88 else if(v_it->is_false())
89 assumptions.push_back(!l.first);
94 assumptions.push_back(!
failed->cond_literal);
107 for(
auto &l : lpoints)
124 v.resize(lpoints.size());
125 for(
size_t i=0; i<lpoints.size(); ++i)
127 for(
size_t i=0; i<v.size(); ++i)
130 if(!
check(lpoints, v))
133 if(!
check(lpoints, v))
146 goal_id=
failed->source.pc->source_location.get_property_id();
169 goal_id=
failed->source.pc->source_location.get_property_id();
176 <<
" unable to localize fault" 181 debug() <<
"Fault localization scores:" <<
eom;
182 lpointt &max=lpoints.begin()->second;
183 for(
auto &l : lpoints)
186 <<
"\n score: " << l.second.score <<
eom;
187 if(max.
score<l.second.score)
191 <<
" " << max.
target->source_location
206 status() <<
"Passing problem to " 226 status() <<
"Runtime decision procedure: " 227 << (sat_stop-sat_start) <<
"s" <<
eom;
253 status() <<
"\n** Most likely fault location:" <<
eom;
260 error() <<
"decision procedure failed" <<
eom;
272 if(g.second.status==goalt::statust::FAILURE)
276 for(
auto &c : g.second.instances)
282 g.second.status=goalt::statust::FAILURE;
283 symex_target_equationt::SSA_stepst::iterator next=c;
286 g.second.goto_trace);
307 status() <<
"\n** Most likely fault location:" <<
eom;
310 if(g.second.status!=goalt::statust::FAILURE)
safety_checkert::resultt stop_on_fail()
goto_programt::const_targett target
const std::string & id2string(const irep_idt &d)
safety_checkert::resultt operator()()
bool check(const lpointst &lpoints, const lpoints_valuet &value)
virtual void report_failure()
static mstreamt & eom(mstreamt &m)
void report(irep_idt goal_id)
virtual void error_trace()
virtual resultt dec_solve()=0
source_locationt source_location
safety_checkert::resultt operator()()
API to expression classes.
bool get_bool_option(const std::string &option) const
std::vector< tvt > lpoints_valuet
virtual void goal_covered(const cover_goalst::goalt &)
virtual void set_message_handler(message_handlert &_message_handler)
std::size_t number_covered() const
void run(irep_idt goal_id)
std::map< literalt, lpointt > lpointst
symex_target_equationt::SSA_stepst::const_iterator failed
decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
absolute_timet current_time()
symex_target_equationt::SSA_stepst::const_iterator get_failed_property()
virtual void report(const cover_goalst &cover_goals)
Try to cover some given set of goals incrementally.
symex_target_equationt equation
virtual void set_frozen(literalt a)
virtual void report_success()
void collect_guards(lpointst &lpoints)
void update_scores(lpointst &lpoints, const lpoints_valuet &value)
std::vector< literalt > bvt
void localize_linear(lpointst &lpoints)
void build_goto_trace(const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
virtual void set_assumptions(const bvt &_assumptions)
Counterexample Beautification.
virtual std::string decision_procedure_text() const =0