cprover
Classes | Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | Protected Member Functions | List of all members
property_checkert Class Referenceabstract

#include <property_checker.h>

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

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 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
}
 

Public Member Functions

 property_checkert ()
 
 property_checkert (message_handlert &_message_handler)
 
virtual resultt operator() (const goto_modelt &)=0
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlert & get_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamt & get_mstream (unsigned message_level)
 
mstreamt & error ()
 
mstreamt & warning ()
 
mstreamt & result ()
 
mstreamt & status ()
 
mstreamt & statistics ()
 
mstreamt & progress ()
 
mstreamt & debug ()
 

Static Public Member Functions

static std::string as_string (resultt)
 
- Static Public Member Functions inherited from messaget
static mstreamt & eom (mstreamt &m)
 
static mstreamt & endl (mstreamt &m)
 

Public Attributes

property_mapt property_map
 

Protected Member Functions

void initialize_property_map (const goto_functionst &)
 

Additional Inherited Members

- Protected Attributes inherited from messaget
message_handlert * message_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 22 of file property_checker.h.

Member Typedef Documentation

◆ property_mapt

typedef std::map<irep_idt, property_statust> property_checkert::property_mapt

Definition at line 48 of file property_checker.h.

Member Enumeration Documentation

◆ resultt

enum property_checkert::resultt
strong
Enumerator
PASS 
FAIL 
ERROR 
UNKNOWN 

Definition at line 32 of file property_checker.h.

Constructor & Destructor Documentation

◆ property_checkert() [1/2]

property_checkert::property_checkert ( )
inline

Definition at line 25 of file property_checker.h.

◆ property_checkert() [2/2]

property_checkert::property_checkert ( message_handlert &  _message_handler)
explicit

Definition at line 27 of file property_checker.cpp.

Member Function Documentation

◆ as_string()

std::string property_checkert::as_string ( resultt  result)
static

Definition at line 14 of file property_checker.cpp.

References ERROR, FAIL, PASS, messaget::result(), and UNKNOWN.

◆ initialize_property_map()

void property_checkert::initialize_property_map ( const goto_functionst &  goto_functions)
protected

Definition at line 33 of file property_checker.cpp.

References goto_functions_templatet< bodyT >::entry_point(), forall_goto_functions, forall_goto_program_instructions, source_locationt::get_property_id(), property_checkert::property_statust::location, property_map, property_checkert::property_statust::result, and UNKNOWN.

◆ operator()()

virtual resultt property_checkert::operator() ( const goto_modelt &  )
pure virtual

Member Data Documentation

◆ property_map

property_mapt property_checkert::property_map

Definition at line 49 of file property_checker.h.

Referenced by initialize_property_map().

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