CBMC
Loading...
Searching...
No Matches
safety_checker.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Safety Checker Interface
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
13#define CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
14
15// this is just an interface -- it won't actually do any checking!
16
17#include <util/invariant.h>
18#include <util/message.h>
19
20#include "goto_trace.h"
21
22class goto_functionst;
23
25{
26public:
28
29 enum class resultt
30 {
32 SAFE,
34 UNSAFE,
36 ERROR,
40 PAUSED,
41 };
42
43 // check whether all assertions in goto_functions are safe
44 // if UNSAFE, then a trace is returned
45
47 const goto_functionst &goto_functions)=0;
48
49 // this is the counterexample
51
52protected:
53 // the namespace
54 const namespacet &ns;
55};
56
84
112#endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A collection of goto functions.
Trace of a GOTO program.
Definition goto_trace.h:177
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const namespacet & ns
@ UNSAFE
Some safety properties were violated.
@ PAUSED
Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the sy...
@ SAFE
No safety properties were violated.
@ ERROR
Safety is unknown due to an error during safety checking.
virtual resultt operator()(const goto_functionst &goto_functions)=0
goto_tracet error_trace
Traces of GOTO Programs.
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.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463