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,
32 message_handlert &_message_handler);
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
70{
74 switch(a)
75 {
77 return a;
79 a = b;
80 return a;
82 a = b == safety_checkert::resultt::ERROR ? b : a;
83 return a;
86 }
88}
89
98{
102 switch(a)
103 {
105 return a;
107 a = b;
108 return a;
110 a = b == safety_checkert::resultt::SAFE ? b : a;
111 return a;
114 }
116}
117#endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
A collection of goto functions.
Trace of a GOTO program.
Definition goto_trace.h:175
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
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:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463