cprover
|
#include <all_properties_class.h>
Classes | |
struct | goalt |
Public Types | |
typedef std::map< irep_idt, goalt > | goal_mapt |
Public Member Functions | |
bmc_all_propertiest (const goto_functionst &_goto_functions, prop_convt &_solver, bmct &_bmc) | |
safety_checkert::resultt | operator() () |
virtual void | goal_covered (const cover_goalst::goalt &) |
![]() | |
virtual void | satisfying_assignment () |
Public Attributes | |
goal_mapt | goal_map |
Protected Member Functions | |
virtual void | report (const cover_goalst &cover_goals) |
virtual void | do_before_solving () |
Protected Attributes | |
const goto_functionst & | goto_functions |
prop_convt & | solver |
bmct & | bmc |
Additional Inherited Members |
Definition at line 19 of file all_properties_class.h.
typedef std::map<irep_idt, goalt> bmc_all_propertiest::goal_mapt |
Definition at line 86 of file all_properties_class.h.
|
inline |
Definition at line 24 of file all_properties_class.h.
|
inlineprotectedvirtual |
Reimplemented in fault_localizationt.
Definition at line 95 of file all_properties_class.h.
|
virtual |
Reimplemented from cover_goalst::observert.
Reimplemented in fault_localizationt.
Definition at line 27 of file all_properties.cpp.
safety_checkert::resultt bmc_all_propertiest::operator() | ( | void | ) |
Definition at line 50 of file all_properties.cpp.
|
protectedvirtual |
Reimplemented in fault_localizationt.
Definition at line 154 of file all_properties.cpp.
|
protected |
Definition at line 92 of file all_properties_class.h.
goal_mapt bmc_all_propertiest::goal_map |
Definition at line 87 of file all_properties_class.h.
|
protected |
Definition at line 90 of file all_properties_class.h.
|
protected |
Definition at line 91 of file all_properties_class.h.