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;
50 
51 protected:
53 };
54 
55 #endif // CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
property_checkert::property_map
property_mapt property_map
Definition: property_checker.h:49
property_checkert::property_statust::location
goto_programt::const_targett location
Definition: property_checker.h:44
goto_model.h
goto_modelt
Definition: goto_model.h:24
property_checkert::operator()
virtual resultt operator()(const goto_modelt &)=0
goto_trace.h
property_checkert::initialize_property_map
void initialize_property_map(const goto_functionst &)
Definition: property_checker.cpp:33
property_checkert::resultt::PASS
property_checkert
Definition: property_checker.h:22
message_handlert
Definition: message.h:24
property_checkert::property_mapt
std::map< irep_idt, property_statust > property_mapt
Definition: property_checker.h:48
property_checkert::property_checkert
property_checkert()
Definition: property_checker.h:25
property_checkert::resultt::FAIL
property_checkert::property_statust::result
resultt result
Definition: property_checker.h:43
property_checkert::property_statust
Definition: property_checker.h:39
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
property_checkert::resultt::ERROR
property_checkert::resultt::UNKNOWN
property_checkert::as_string
static std::string as_string(resultt)
Definition: property_checker.cpp:14
goto_tracet
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
message.h
property_checkert::resultt
resultt
Definition: property_checker.h:32
property_checkert::property_statust::error_trace
goto_tracet error_trace
Definition: property_checker.h:42