cprover
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:
27 explicit safety_checkert(
28 const namespacet &_ns);
29
30 explicit safety_checkert(
31 const namespacet &_ns,
33
34 enum class resultt
35 {
37 SAFE,
39 UNSAFE,
41 ERROR,
45 PAUSED,
46 };
47
48 // check whether all assertions in goto_functions are safe
49 // if UNSAFE, then a trace is returned
50
52 const goto_functionst &goto_functions)=0;
53
54 // this is the counterexample
56
57protected:
58 // the namespace
59 const namespacet &ns;
60};
61
89
117#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:563
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:155
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
safety_checkert(const namespacet &_ns)
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