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/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, [email protected]
 #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