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/message.h>
18 
19 #include "goto_trace.h"
20 #include "goto_functions.h"
21 
23 {
24 public:
25  explicit safety_checkert(
26  const namespacet &_ns);
27 
28  explicit safety_checkert(
29  const namespacet &_ns,
30  message_handlert &_message_handler);
31 
32  enum class resultt { SAFE, UNSAFE, ERROR };
33 
34  // check whether all assertions in goto_functions are safe
35  // if UNSAFE, then a trace is returned
36 
37  virtual resultt operator()(
38  const goto_functionst &goto_functions)=0;
39 
40  // this is the counterexample
42 
43 protected:
44  // the namespace
45  const namespacet &ns;
46 };
47 
48 #endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
Goto Programs with Functions.
Traces of GOTO Programs.
safety_checkert(const namespacet &_ns)
goto_tracet error_trace
const namespacet & ns
virtual resultt operator()(const goto_functionst &goto_functions)=0
TO_BE_DOCUMENTED.
Definition: namespace.h:62
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146