Add properties_result_from_symex_target_equation

Updates the property infos with properties
created by goto-symex and sets the status
of already determined properies.

Author: peterschrammel

src/goto-checker/bmc_util.cpp

@@ -225,3 +225,53 @@ void slice(
                    << " remaining after simplification" << messaget::eom;
 }
 
+std::vector<irep_idt> update_properties_status_from_symex_target_equation(
+  propertiest &properties,
+  const symex_target_equationt &equation)
+{
+  std::vector<irep_idt> updated_properties;
+
+  for(const auto &step : equation.SSA_steps)
+  {
+    if(!step.is_assert())
+      continue;
+
+    irep_idt property_id = step.get_property_id();
+
+    if(property_id.empty())
+      continue;
+
+    // Don't set false properties; we wouldn't have traces for them.
+    const auto status = step.cond_expr.is_true() ? property_statust::PASS
+                                                 : property_statust::UNKNOWN;
+    auto emplace_result = properties.emplace(
+      property_id, property_infot{step.source.pc, step.comment, status});
+
+    if(emplace_result.second)
+    {
+      updated_properties.push_back(property_id);
+    }
+    else
+    {
+      property_infot &property_info = emplace_result.first->second;
+      property_statust old_status = property_info.status;
+      property_info.status |= status;
+
+      if(property_info.status != old_status)
+        updated_properties.push_back(property_id);
+    }
+  }
+
+  for(auto &property_pair : properties)
+  {
+    if(property_pair.second.status == property_statust::NOT_CHECKED)
+    {
+      // This could be a NOT_CHECKED, NOT_REACHABLE or PASS,
+      // but the equation doesn't give us precise information.
+      property_pair.second.status = property_statust::PASS;
+      updated_properties.push_back(property_pair.first);
+    }
+  }
+
+  return updated_properties;
+}

src/goto-checker/bmc_util.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-programs/safety_checker.h>
 
+#include "properties.h"
+
 class goto_tracet;
 class memory_model_baset;
 class message_handlert;
@@ -67,6 +69,13 @@ void slice(
   const optionst &,
   ui_message_handlert &);
 
+/// Sets property status to PASS for properties whose
+/// conditions are constant true.
+/// \return IDs of updated properties
+std::vector<irep_idt> update_properties_status_from_symex_target_equation(
+  propertiest &properties,
+  const symex_target_equationt &equation);
+
 // clang-format off
 #define OPT_BMC \
   "(program-only)" \