cprover
safety_checker.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Safety Checker Interface
4 
5 Author: 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 #include "goto_functions.h"
22 
24 {
25 public:
26  explicit safety_checkert(
27  const namespacet &_ns);
28 
29  explicit safety_checkert(
30  const namespacet &_ns,
31  message_handlert &_message_handler);
32 
33  enum class resultt
34  {
36  SAFE,
38  UNSAFE,
40  ERROR,
44  PAUSED,
48  UNKNOWN
49  };
50 
51  // check whether all assertions in goto_functions are safe
52  // if UNSAFE, then a trace is returned
53 
54  virtual resultt operator()(
55  const goto_functionst &goto_functions)=0;
56 
57  // this is the counterexample
59 
60 protected:
61  // the namespace
62  const namespacet &ns;
63 };
64 
73 {
77  switch(a)
78  {
80  a = b;
81  return a;
83  return a;
85  a = b;
86  return a;
88  a = b == safety_checkert::resultt::ERROR ? b : a;
89  return a;
92  }
94 }
95 
104 {
105  PRECONDITION(
108  switch(a)
109  {
111  a = b;
112  return a;
114  return a;
116  a = b;
117  return a;
119  a = b == safety_checkert::resultt::SAFE ? b : a;
120  return a;
122  UNREACHABLE;
123  }
124  UNREACHABLE;
125 }
126 #endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
Goto Programs with Functions.
Traces of GOTO Programs.
safety_checkert(const namespacet &_ns)
We haven&#39;t yet assigned a safety check result to this object.
goto_tracet error_trace
const namespacet & ns
Some safety properties were violated.
Safety is unknown due to an error during safety checking.
virtual resultt operator()(const goto_functionst &goto_functions)=0
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
No safety properties were violated.
Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the sy...
#define UNREACHABLE
Definition: invariant.h:271
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152
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.