cprover
|
#include <property_checker.h>
Classes | |
struct | property_statust |
Public Types | |
enum | resultt { resultt::PASS, resultt::FAIL, resultt::ERROR, resultt::UNKNOWN } |
typedef std::map< irep_idt, property_statust > | property_mapt |
Public Member Functions | |
property_checkert () | |
property_checkert (message_handlert &_message_handler) | |
virtual resultt | operator() (const goto_modelt &)=0 |
Static Public Member Functions | |
static std::string | as_string (resultt) |
Public Attributes | |
property_mapt | property_map |
Protected Member Functions | |
void | initialize_property_map (const goto_functionst &) |
Additional Inherited Members |
Definition at line 22 of file property_checker.h.
typedef std::map<irep_idt, property_statust> property_checkert::property_mapt |
Definition at line 48 of file property_checker.h.
|
strong |
Enumerator | |
---|---|
PASS | |
FAIL | |
ERROR | |
UNKNOWN |
Definition at line 32 of file property_checker.h.
|
inline |
Definition at line 25 of file property_checker.h.
|
explicit |
Definition at line 27 of file property_checker.cpp.
|
static |
Definition at line 14 of file property_checker.cpp.
References ERROR, FAIL, PASS, messaget::result(), and UNKNOWN.
|
protected |
Definition at line 33 of file property_checker.cpp.
References goto_functionst::entry_point(), forall_goto_functions, forall_goto_program_instructions, source_locationt::get_property_id(), goto_program, property_checkert::property_statust::location, property_map, property_checkert::property_statust::result, and UNKNOWN.
|
pure virtual |
property_mapt property_checkert::property_map |
Definition at line 49 of file property_checker.h.
Referenced by initialize_property_map().