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,
45  };
46 
47  // check whether all assertions in goto_functions are safe
48  // if UNSAFE, then a trace is returned
49 
51  const goto_functionst &goto_functions)=0;
52 
53  // this is the counterexample
55 
56 protected:
57  // the namespace
58  const namespacet &ns;
59 };
60 
69 {
73  switch(a)
74  {
76  return a;
78  a = b;
79  return a;
81  a = b == safety_checkert::resultt::ERROR ? b : a;
82  return a;
85  }
87 }
88 
97 {
101  switch(a)
102  {
104  return a;
106  a = b;
107  return a;
109  a = b == safety_checkert::resultt::SAFE ? b : a;
110  return a;
112  UNREACHABLE;
113  }
114  UNREACHABLE;
115 }
116 #endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
safety_checkert::resultt::PAUSED
@ PAUSED
Symbolic execution has been suspended due to encountering a GOTO while doing path exploration; the sy...
safety_checkert::resultt::SAFE
@ SAFE
No safety properties were violated.
invariant.h
safety_checkert::safety_checkert
safety_checkert(const namespacet &_ns)
Definition: safety_checker.cpp:14
goto_trace.h
Traces of GOTO Programs.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
safety_checkert::ns
const namespacet & ns
Definition: safety_checker.h:58
safety_checkert::error_trace
goto_tracet error_trace
Definition: safety_checker.h:54
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
message_handlert
Definition: message.h:28
safety_checkert::resultt::ERROR
@ ERROR
Safety is unknown due to an error during safety checking.
safety_checkert::resultt::UNSAFE
@ UNSAFE
Some safety properties were violated.
safety_checkert::operator()
virtual resultt operator()(const goto_functionst &goto_functions)=0
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
safety_checkert::resultt
resultt
Definition: safety_checker.h:34
safety_checkert
Definition: safety_checker.h:24
operator&=
safety_checkert::resultt & operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
The worst of two results.
Definition: safety_checker.h:68
goto_functions.h
Goto Programs with Functions.
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
operator|=
safety_checkert::resultt & operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
The best of two results.
Definition: safety_checker.h:96
message.h