cprover
property_checker.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Property Checker Interface
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
13 #define CPROVER_GOTO_PROGRAMS_PROPERTY_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_model.h"
21 
23 {
24 public:
26  {
27  }
28 
29  explicit property_checkert(
30  message_handlert &_message_handler);
31 
32  enum class resultt { PASS, FAIL, ERROR, UNKNOWN };
33 
34  static std::string as_string(resultt);
35 
36  // Check whether all properties in goto_functions hold.
37  virtual resultt operator()(const goto_modelt &)=0;
38 
40  {
41  // this is the counterexample
45  };
46 
47  // the irep_idt is the property id
48  typedef std::map<irep_idt, property_statust> property_mapt;
49  property_mapt property_map;
50 
51 protected:
53 };
54 
55 #endif // CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
std::map< irep_idt, property_statust > property_mapt
Traces of GOTO Programs.
void initialize_property_map(const goto_functionst &)
static std::string as_string(resultt)
Symbol Table + CFG.
instructionst::const_iterator const_targett
property_mapt property_map
virtual resultt operator()(const goto_modelt &)=0
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
goto_programt::const_targett location