12 #ifndef CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H 13 #define CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H 126 #endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
Goto Programs with Functions.
safety_checkert(const namespacet &_ns)
We haven't yet assigned a safety check result to this object.
Some safety properties were violated.
Safety is unknown due to an error during safety checking.
virtual resultt operator()(const goto_functionst &goto_functions)=0
#define PRECONDITION(CONDITION)
No safety properties were violated.
Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the sy...
safety_checkert::resultt & operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
The best of two results.
safety_checkert::resultt & operator &=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
The worst of two results.