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)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

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)
 
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)
 
xmlt report_xml (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 unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Public Attributes inherited from bmc_all_propertiest
goal_mapt goal_map
 

Detailed Description

Definition at line 24 of file fault_localization.h.

Member Typedef Documentation

◆ lpoints_mapt

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

Definition at line 62 of file fault_localization.h.

◆ lpoints_valuet

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

Definition at line 73 of file fault_localization.h.

◆ lpointst

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

Definition at line 61 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 43 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 123 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]

◆ report_xml()

◆ run()

◆ run_decision_procedure()

◆ stop_on_fail()

◆ update_scores()

void fault_localizationt::update_scores ( lpointst lpoints)
protected

Definition at line 107 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 53 of file fault_localization.h.

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

◆ goto_functions

const goto_functionst& fault_localizationt::goto_functions
protected

Definition at line 48 of file fault_localization.h.

◆ lpoints_map

lpoints_mapt fault_localizationt::lpoints_map
protected

Definition at line 63 of file fault_localization.h.

Referenced by report(), report_xml(), and run().

◆ options

const optionst& fault_localizationt::options
protected

Definition at line 50 of file fault_localization.h.

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


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