Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
13 #define CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
116 #endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
Class that provides messages with a built-in verbosity 'level'.
#define PRECONDITION(CONDITION)
Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the sy...
No safety properties were violated.
safety_checkert(const namespacet &_ns)
#define UNREACHABLE
This should be used to mark dead code.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Safety is unknown due to an error during safety checking.
Some safety properties were violated.
virtual resultt operator()(const goto_functionst &goto_functions)=0
A collection of goto functions.
safety_checkert::resultt & operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
The worst of two results.
safety_checkert::resultt & operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
The best of two results.