cprover
|
#include <safety_checker.h>
Public Types | |
enum | resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR } |
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 Attributes | |
goto_tracet | error_trace |
Protected Attributes | |
const namespacet & | ns |
Additional Inherited Members |
Definition at line 22 of file safety_checker.h.
|
strong |
Enumerator | |
---|---|
SAFE | |
UNSAFE | |
ERROR |
Definition at line 32 of file safety_checker.h.
|
explicit |
Definition at line 14 of file safety_checker.cpp.
|
explicit |
Definition at line 19 of file safety_checker.cpp.
|
pure virtual |
Implemented in bmct, and path_searcht.
goto_tracet safety_checkert::error_trace |
Definition at line 41 of file safety_checker.h.
Referenced by bmct::error_trace(), and bmct::output_graphml().
|
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()().