35 if(!step.guard_literal.is_constant())
37 if(step.is_assert() &&
38 !step.cond_literal.is_constant())
45 for(symex_target_equationt::SSA_stepst::const_iterator
49 if(it->is_assignment() &&
53 if(!it->guard_literal.is_constant())
55 lpoints[it->guard_literal].target=it->source.pc;
56 lpoints[it->guard_literal].score=0;
66 symex_target_equationt::SSA_stepst::const_iterator
69 for(symex_target_equationt::SSA_stepst::const_iterator
84 assert(value.size()==lpoints.size());
86 lpoints_valuet::const_iterator v_it=value.begin();
87 for(
const auto &l : lpoints)
90 assumptions.push_back(l.first);
91 else if(v_it->is_false())
92 assumptions.push_back(!l.first);
97 assumptions.push_back(!
failed->cond_literal);
110 for(
auto &l : lpoints)
127 v.resize(lpoints.size());
128 for(
size_t i=0; i<lpoints.size(); ++i)
130 for(
size_t i=0; i<v.size(); ++i)
133 if(!
check(lpoints, v))
136 if(!
check(lpoints, v))
149 goal_id=
failed->source.pc->source_location.get_property_id();
172 goal_id=
failed->source.pc->source_location.get_property_id();
179 <<
" unable to localize fault" 184 debug() <<
"Fault localization scores:" <<
eom;
185 lpointt &max=lpoints.begin()->second;
186 for(
auto &l : lpoints)
189 <<
"\n score: " << l.second.score <<
eom;
190 if(max.
score<l.second.score)
194 <<
" " << max.
target->source_location
200 xmlt xml_diagnosis(
"diagnosis");
204 goal_id=
failed->source.pc->source_location.get_property_id();
213 return xml_diagnosis;
216 debug() <<
"Fault localization scores:" <<
eom;
217 const lpointt *max=&lpoints.begin()->second;
218 for(
const auto &pair : lpoints)
220 const auto &value=pair.second;
222 <<
"\n score: " << value.score <<
eom;
223 if(max->
score<value.score)
230 return xml_diagnosis;
244 status() <<
"Passing problem to " 249 auto solver_start=std::chrono::steady_clock::now();
262 auto solver_stop=std::chrono::steady_clock::now();
263 status() <<
"Runtime decision procedure: " 264 << std::chrono::duration<double>(solver_stop-solver_start).count()
296 status() <<
"\n** Most likely fault location:" <<
eom;
302 xmlt dest(
"fault-localization");
317 error() <<
"decision procedure failed" <<
eom;
329 if(goal_pair.second.status==goalt::statust::FAILURE)
333 for(
auto &inst : goal_pair.second.instances)
339 goal_pair.second.status=goalt::statust::FAILURE;
340 symex_target_equationt::SSA_stepst::iterator next=inst;
346 run(goal_pair.first);
364 status() <<
"\n** Most likely fault location:" <<
eom;
367 if(goal_pair.second.status!=goalt::statust::FAILURE)
375 xmlt dest(
"fault-localization");
378 if(goal_pair.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()
xmlt report_xml(irep_idt goal_id)
static mstreamt & eom(mstreamt &m)
xmlt xml(const source_locationt &location)
void report(irep_idt goal_id)
virtual void error_trace()
virtual resultt dec_solve()=0
Some safety properties were violated.
ui_message_handlert::uit ui
source_locationt source_location
Safety is unknown due to an error during safety checking.
safety_checkert::resultt operator()()
API to expression classes.
bool get_bool_option(const std::string &option) const
void set_attribute(const std::string &attribute, unsigned value)
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
No safety properties were violated.
xmlt & new_element(const std::string &name)
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)
decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
mstreamt & status() const
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)
virtual void set_assumptions(const bvt &_assumptions)
Counterexample Beautification.
virtual std::string decision_procedure_text() const =0