12 #ifndef CPROVER_CBMC_FAULT_LOCALIZATION_H 13 #define CPROVER_CBMC_FAULT_LOCALIZATION_H 54 symex_target_equationt::SSA_stepst::const_iterator
failed;
75 bool check(
const lpointst &lpoints,
const lpoints_valuet &value);
77 const lpoints_valuet &value);
103 #endif // CPROVER_CBMC_FAULT_LOCALIZATION_H
safety_checkert::resultt stop_on_fail()
goto_programt::const_targett target
Generate Equation using Symbolic Execution.
bool check(const lpointst &lpoints, const lpoints_valuet &value)
fault_localizationt(const goto_functionst &_goto_functions, bmct &_bmc, const optionst &_options)
void report(irep_idt goal_id)
instructionst::const_iterator const_targett
safety_checkert::resultt operator()()
virtual void do_before_solving()
std::vector< tvt > lpoints_valuet
virtual void goal_covered(const cover_goalst::goalt &)
virtual void set_message_handler(message_handlert &_message_handler)
Symbolic Execution of ANSI-C.
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)
message_handlert & get_message_handler()
Bounded Model Checking for ANSI-C + HDL.
std::map< irep_idt, lpointst > lpoints_mapt
const goto_functionst & goto_functions
symex_target_equationt::SSA_stepst::const_iterator get_failed_property()
Try to cover some given set of goals incrementally.
void collect_guards(lpointst &lpoints)
void update_scores(lpointst &lpoints, const lpoints_valuet &value)
void localize_linear(lpointst &lpoints)