cprover
safety_checkert Class Referenceabstract

#include <safety_checker.h>

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

Public Types

enum  resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR }
 
- 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

 safety_checkert (const namespacet &_ns)
 
 safety_checkert (const namespacet &_ns, message_handlert &_message_handler)
 
virtual resultt operator() (const goto_functionst &goto_functions)=0
 
- 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 ()
 

Public Attributes

goto_tracet error_trace
 

Protected Attributes

const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 22 of file safety_checker.h.

Member Enumeration Documentation

§ resultt

Enumerator
SAFE 
UNSAFE 
ERROR 

Definition at line 32 of file safety_checker.h.

Constructor & Destructor Documentation

§ safety_checkert() [1/2]

safety_checkert::safety_checkert ( const namespacet _ns)
explicit

Definition at line 14 of file safety_checker.cpp.

§ safety_checkert() [2/2]

safety_checkert::safety_checkert ( const namespacet _ns,
message_handlert _message_handler 
)
explicit

Definition at line 19 of file safety_checker.cpp.

Member Function Documentation

§ operator()()

virtual resultt safety_checkert::operator() ( const goto_functionst goto_functions)
pure virtual

Implemented in bmct, and path_searcht.

Member Data Documentation

§ error_trace

goto_tracet safety_checkert::error_trace

Definition at line 41 of file safety_checker.h.

Referenced by bmct::error_trace(), and bmct::output_graphml().

§ ns


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