Go to the documentation of this file.
12 #ifndef CPROVER_CBMC_FAULT_LOCALIZATION_H
13 #define CPROVER_CBMC_FAULT_LOCALIZATION_H
53 symex_target_equationt::SSA_stepst::const_iterator
failed;
103 #endif // CPROVER_CBMC_FAULT_LOCALIZATION_H
std::vector< tvt > lpoints_valuet
xmlt report_xml(irep_idt goal_id)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Bounded model checking or path exploration for goto-programs.
void report(irep_idt goal_id)
void run(irep_idt goal_id)
void collect_guards(lpointst &lpoints)
safety_checkert::resultt operator()()
void localize_linear(lpointst &lpoints)
symex_target_equationt::SSA_stepst::const_iterator get_failed_property()
Try to cover some given set of goals incrementally.
symex_target_equationt::SSA_stepst::const_iterator failed
const goto_functionst & goto_functions
std::map< irep_idt, lpointst > lpoints_mapt
goto_programt::const_targett target
virtual void do_before_solving()
virtual void set_message_handler(message_handlert &_message_handler)
virtual void goal_covered(const cover_goalst::goalt &)
A collection of goto functions.
safety_checkert::resultt stop_on_fail()
message_handlert & get_message_handler()
instructionst::const_iterator const_targett
fault_localizationt(const goto_functionst &_goto_functions, bmct &_bmc, const optionst &_options)
std::map< literalt, lpointt > lpointst
decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
void update_scores(lpointst &lpoints)
bool check(const lpointst &lpoints, const lpoints_valuet &value)