Add a version of static_verifier that works with propertiest

This will make it easier to use with static_verifiert going forward.

Author: hannes-steffenhagen-diffblue

src/goto-analyzer/CMakeLists.txt

@@ -12,6 +12,7 @@ target_link_libraries(goto-analyzer-lib
     cpp
     linking
     big-int
+    goto-checker
     goto-programs
     analyses
     pointer-analysis

src/goto-analyzer/Makefile

@@ -13,6 +13,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
+      ../goto-checker/goto-checker$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../pointer-analysis/pointer-analysis$(LIBEXT) \

src/goto-analyzer/module_dependencies.txt

@@ -3,6 +3,7 @@ analyses
 assembler
 cpp
 goto-analyzer
+goto-checker
 goto-programs
 java_bytecode # will go away
 langapi # should go away

src/goto-analyzer/static_verifier.cpp

@@ -27,6 +27,39 @@ struct static_verifier_resultt
   irep_idt function_id;
 };
 
+void static_verifier(
+  const abstract_goto_modelt &abstract_goto_model,
+  const ai_baset &ai,
+  propertiest &properties)
+{
+  auto const ns = namespacet{abstract_goto_model.get_symbol_table()};
+  for(auto &property : properties)
+  {
+    auto &property_status = property.second.status;
+    auto const &property_location = property.second.pc;
+    auto condition = property_location->get_condition();
+    auto const predecessor = ai.abstract_state_before(property_location);
+    auto const &domain = *predecessor;
+    domain.ai_simplify(condition, ns);
+    if(condition.is_true())
+    {
+      property_status = property_statust::PASS;
+    }
+    else if(condition.is_false())
+    {
+      property_status = property_statust::FAIL;
+    }
+    else if(domain.is_bottom())
+    {
+      property_status = property_statust::NOT_REACHABLE;
+    }
+    else
+    {
+      property_status = property_statust::UNKNOWN;
+    }
+  }
+}
+
 /// Makes a status message string from a status.
 static const char *message(const static_verifier_resultt::statust &status)
 {

src/goto-analyzer/static_verifier.h

@@ -9,6 +9,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 #ifndef CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
 #define CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
 
+#include <goto-checker/properties.h>
+#include <goto-programs/abstract_goto_model.h>
 #include <iosfwd>
 
 class ai_baset;
@@ -23,4 +25,9 @@ bool static_verifier(
   message_handlert &,
   std::ostream &);
 
+void static_verifier(
+  const abstract_goto_modelt &abstract_goto_model,
+  const ai_baset &ai,
+  propertiest &properties);
+
 #endif // CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H