safety_checkert Class Reference

#include <safety_checker.h>

Inheritance diagram for safety_checkert:

Collaboration diagram for safety_checkert:

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

Public Attributes
goto_tracet	error_trace

Protected Attributes
const namespacet &	ns
Protected Attributes inherited from messaget
message_handlert *	message_handler
mstreamt	mstream

Additional Inherited Members
Static Public Member Functions inherited from messaget
static mstreamt &	eom (mstreamt &m)
static mstreamt &	endl (mstreamt &m)

Detailed Description

Definition at line 22 of file safety_checker.h.

Member Enumeration Documentation

resultt

enum safety_checkert::resultt

strong

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

const namespacet& safety_checkert::ns

protected

Definition at line 45 of file safety_checker.h.

Referenced by path_searcht::check_assertion(), path_searcht::do_show_vcc(), path_searcht::drop_state(), path_searcht::is_feasible(), and path_searcht::operator()().

---

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

• goto-programs/safety_checker.h
• goto-programs/safety_checker.cpp