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, resultt::PAUSED,
  resultt::UNKNOWN
}
 
- 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)
 
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...
 

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

Detailed Description

Definition at line 23 of file safety_checker.h.

Member Enumeration Documentation

◆ resultt

Enumerator
SAFE 

No safety properties were violated.

UNSAFE 

Some safety properties were violated.

ERROR 

Safety is unknown due to an error during safety checking.

PAUSED 

Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the symex state has been saved, and symex should be resumed by the caller.

UNKNOWN 

We haven't yet assigned a safety check result to this object.

A value of UNKNOWN can be used to initialize a resultt object, and that object may then safely be used with the |= and &= operators.

Definition at line 33 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.

Member Data Documentation

◆ error_trace

goto_tracet safety_checkert::error_trace

Definition at line 58 of file safety_checker.h.

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

◆ ns

const namespacet& safety_checkert::ns
protected

Definition at line 62 of file safety_checker.h.


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