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
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);
109 for(
auto &l : lpoints)
126 v.resize(lpoints.size());
127 for(
size_t i=0; i<lpoints.size(); ++i)
129 for(
size_t i=0; i<v.size(); ++i)
132 if(!
check(lpoints, v))
135 if(!
check(lpoints, v))
148 goal_id=
failed->source.pc->source_location.get_property_id();
171 goal_id=
failed->source.pc->source_location.get_property_id();
178 <<
" unable to localize fault" 183 debug() <<
"Fault localization scores:" <<
eom;
184 lpointt &max=lpoints.begin()->second;
185 for(
auto &l : lpoints)
188 <<
"\n score: " << l.second.score <<
eom;
189 if(max.
score<l.second.score)
193 <<
" " << max.
target->source_location
199 xmlt xml_diagnosis(
"diagnosis");
203 goal_id=
failed->source.pc->source_location.get_property_id();
212 return xml_diagnosis;
215 debug() <<
"Fault localization scores:" <<
eom;
216 const lpointt *max=&lpoints.begin()->second;
217 for(
const auto &pair : lpoints)
219 const auto &value=pair.second;
221 <<
"\n score: " << value.score <<
eom;
222 if(max->
score<value.score)
229 return xml_diagnosis;
243 status() <<
"Passing problem to " 248 auto solver_start=std::chrono::steady_clock::now();
261 auto solver_stop=std::chrono::steady_clock::now();
262 status() <<
"Runtime decision procedure: " 263 << std::chrono::duration<double>(solver_stop-solver_start).count()
295 status() <<
"\n** Most likely fault location:" <<
eom;
301 xmlt dest(
"fault-localization");
316 error() <<
"decision procedure failed" <<
eom;
328 if(goal_pair.second.status==goalt::statust::FAILURE)
332 for(
auto &inst : goal_pair.second.instances)
338 goal_pair.second.status=goalt::statust::FAILURE;
343 run(goal_pair.first);
361 status() <<
"\n** Most likely fault location:" <<
eom;
364 if(goal_pair.second.status!=goalt::statust::FAILURE)
372 xmlt dest(
"fault-localization");
375 if(goal_pair.second.status!=goalt::statust::FAILURE)
safety_checkert::resultt stop_on_fail()
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
goto_programt::const_targett target
ui_message_handlert & ui_message_handler
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)
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.
void update_scores(lpointst &lpoints)
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 &)
#define PRECONDITION(CONDITION)
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
No safety properties were violated.
decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
xmlt & new_element(const std::string &key)
mstreamt & status() const
symex_target_equationt::SSA_stepst::const_iterator get_failed_property()
virtual void report(const cover_goalst &cover_goals)
#define UNREACHABLE
This should be used to mark dead code.
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)
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