#include <safety_checker.h>
|
enum | resultt {
resultt::SAFE,
resultt::UNSAFE,
resultt::ERROR,
resultt::PAUSED,
resultt::UNKNOWN
} |
|
enum | message_levelt {
M_ERROR =1,
M_WARNING =2,
M_RESULT =4,
M_STATUS =6,
M_STATISTICS =8,
M_PROGRESS =9,
M_DEBUG =10
} |
|
Definition at line 23 of file safety_checker.h.
◆ 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.
◆ safety_checkert() [1/2]
safety_checkert::safety_checkert |
( |
const namespacet & |
_ns | ) |
|
|
explicit |
◆ safety_checkert() [2/2]
◆ operator()()
◆ error_trace
◆ ns
The documentation for this class was generated from the following files: