property_checkert interface

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3910 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/goto-programs/Makefile

@@ -1,6 +1,6 @@
 SRC = goto_convert.cpp goto_convert_function_call.cpp \
       goto_convert_side_effect.cpp goto_program.cpp basic_blocks.cpp \
-      goto_convert_exceptions.cpp \
+      goto_convert_exceptions.cpp property_checker.cpp \
       remove_function_pointers.cpp goto_functions.cpp goto_inline.cpp \
       remove_skip.cpp goto_convert_functions.cpp string_instrumentation.cpp \
       builtin_functions.cpp show_properties.cpp set_properties.cpp \

src/goto-programs/property_checker.cpp

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: Property Checker Interface
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "property_checker.h"
+
+/*******************************************************************\
+
+Function: property_checkert::property_checkert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+property_checkert::property_checkert(
+  message_handlert &_message_handler):
+  messaget(_message_handler)
+{
+}
+

src/goto-programs/property_checker.h

@@ -0,0 +1,46 @@
+/*******************************************************************\
+
+Module: Property Checker Interface
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_PROPERTY_CHECKER_H
+#define CPROVER_PROPERTY_CHECKER_H
+
+// this is just an interface -- it won't actually do any checking!
+
+#include <util/message.h>
+
+#include "goto_trace.h"
+#include "goto_model.h"
+
+class property_checkert:public messaget
+{
+public:
+  property_checkert();
+
+  explicit property_checkert(
+    message_handlert &_message_handler);
+
+  typedef enum { PASS, FAIL, ERROR } resultt;
+
+  // Check whether all properties in goto_functions hold.
+
+  virtual resultt operator()(
+    const goto_modelt &goto_model)=0;
+
+  struct property_statust
+  {
+    // this is the counterexample  
+    goto_tracet error_trace;
+    resultt result;
+  };
+  
+  typedef goto_programt::const_targett loct;
+  typedef std::map<loct, property_statust> property_mapt;
+  property_mapt property_map;
+};
+
+#endif