cprover
fault_localizationt Class Reference

#include <fault_localization.h>

Inheritance diagram for fault_localizationt:
[legend]
Collaboration diagram for fault_localizationt:
[legend]

Classes

struct  lpointt
 

Public Member Functions

 fault_localizationt (const goto_functionst &_goto_functions, bmct &_bmc, const optionst &_options)
 
safety_checkert::resultt operator() ()
 
safety_checkert::resultt stop_on_fail ()
 
virtual void goal_covered (const cover_goalst::goalt &)
 
- Public Member Functions inherited from bmc_all_propertiest
 bmc_all_propertiest (const goto_functionst &_goto_functions, prop_convt &_solver, bmct &_bmc)
 
safety_checkert::resultt operator() ()
 
- Public Member Functions inherited from cover_goalst::observert
virtual void satisfying_assignment ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Protected Types

typedef std::map< literalt, lpointtlpointst
 
typedef std::map< irep_idt, lpointstlpoints_mapt
 
typedef std::vector< tvtlpoints_valuet
 

Protected Member Functions

void run (irep_idt goal_id)
 
void collect_guards (lpointst &lpoints)
 
void freeze_guards ()
 
bool check (const lpointst &lpoints, const lpoints_valuet &value)
 
void update_scores (lpointst &lpoints, const lpoints_valuet &value)
 
void localize_linear (lpointst &lpoints)
 
symex_target_equationt::SSA_stepst::const_iterator get_failed_property ()
 
decision_proceduret::resultt run_decision_procedure (prop_convt &prop_conv)
 
void report (irep_idt goal_id)
 
virtual void report (const cover_goalst &cover_goals)
 
virtual void do_before_solving ()
 

Protected Attributes

const goto_functionstgoto_functions
 
bmctbmc
 
const optionstoptions
 
symex_target_equationt::SSA_stepst::const_iterator failed
 
lpoints_mapt lpoints_map
 
- Protected Attributes inherited from bmc_all_propertiest
const goto_functionstgoto_functions
 
prop_convtsolver
 
bmctbmc
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Public Types inherited from bmc_all_propertiest
typedef std::map< irep_idt, goaltgoal_mapt
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Public Attributes inherited from bmc_all_propertiest
goal_mapt goal_map
 

Detailed Description

Definition at line 25 of file fault_localization.h.

Member Typedef Documentation

◆ lpoints_mapt

typedef std::map<irep_idt, lpointst> fault_localizationt::lpoints_mapt
protected

Definition at line 63 of file fault_localization.h.

◆ lpoints_valuet

typedef std::vector<tvt> fault_localizationt::lpoints_valuet
protected

Definition at line 74 of file fault_localization.h.

◆ lpointst

typedef std::map<literalt, lpointt> fault_localizationt::lpointst
protected

Definition at line 62 of file fault_localization.h.

Constructor & Destructor Documentation

◆ fault_localizationt()

fault_localizationt::fault_localizationt ( const goto_functionst _goto_functions,
bmct _bmc,
const optionst _options 
)
inlineexplicit

Member Function Documentation

◆ check()

bool fault_localizationt::check ( const lpointst lpoints,
const lpoints_valuet value 
)
protected

◆ collect_guards()

void fault_localizationt::collect_guards ( lpointst lpoints)
protected

Definition at line 40 of file fault_localization.cpp.

References bmc, bmct::equation, failed, symex_target_equationt::SSA_steps, and symex_targett::STATE.

Referenced by run().

◆ do_before_solving()

virtual void fault_localizationt::do_before_solving ( )
inlineprotectedvirtual

Reimplemented from bmc_all_propertiest.

Definition at line 97 of file fault_localization.h.

References freeze_guards().

◆ freeze_guards()

void fault_localizationt::freeze_guards ( )
protected

◆ get_failed_property()

symex_target_equationt::SSA_stepst::const_iterator fault_localizationt::get_failed_property ( )
protected

◆ goal_covered()

void fault_localizationt::goal_covered ( const cover_goalst::goalt )
virtual

◆ localize_linear()

void fault_localizationt::localize_linear ( lpointst lpoints)
protected

Definition at line 121 of file fault_localization.cpp.

References check(), tvt::TV_FALSE, tvt::TV_TRUE, tvt::TV_UNKNOWN, and update_scores().

Referenced by run().

◆ operator()()

safety_checkert::resultt fault_localizationt::operator() ( void  )

◆ report() [1/2]

◆ report() [2/2]

◆ run()

◆ run_decision_procedure()

◆ stop_on_fail()

◆ update_scores()

void fault_localizationt::update_scores ( lpointst lpoints,
const lpoints_valuet value 
)
protected

Definition at line 104 of file fault_localization.cpp.

References bmc, tvt::is_false(), tvt::is_true(), prop_convt::l_get(), and bmct::prop_conv.

Referenced by localize_linear().

Member Data Documentation

◆ bmc

◆ failed

symex_target_equationt::SSA_stepst::const_iterator fault_localizationt::failed
protected

Definition at line 54 of file fault_localization.h.

Referenced by check(), collect_guards(), report(), and run().

◆ goto_functions

const goto_functionst& fault_localizationt::goto_functions
protected

Definition at line 49 of file fault_localization.h.

◆ lpoints_map

lpoints_mapt fault_localizationt::lpoints_map
protected

Definition at line 64 of file fault_localization.h.

Referenced by report(), and run().

◆ options

const optionst& fault_localizationt::options
protected

Definition at line 51 of file fault_localization.h.

Referenced by operator()(), and stop_on_fail().


The documentation for this class was generated from the following files: