Set final status of UNKNOWN properties

Utility function to set all UNKNOWN properties to PASS
when the verification algorithm has finished.
Corresponds to the current behaviour of CBMC replying
'successful' when the given bounds have been reached.

Author: peterschrammel

src/goto-checker/bmc_util.cpp

@@ -270,6 +270,22 @@ void update_status_of_not_checked_properties(
   }
 }
 
+void update_status_of_unknown_properties(
+  propertiest &properties,
+  std::unordered_set<irep_idt> &updated_properties)
+{
+  for(auto &property_pair : properties)
+  {
+    if(property_pair.second.status == property_statust::UNKNOWN)
+    {
+      // This could have any status except NOT_CHECKED.
+      // We consider them PASS because we do verification modulo bounds.
+      property_pair.second.status = property_statust::PASS;
+      updated_properties.insert(property_pair.first);
+    }
+  }
+}
+
 void output_coverage_report(
   const std::string &cov_out,
   const abstract_goto_modelt &goto_model,

src/goto-checker/bmc_util.h

@@ -124,6 +124,16 @@ void update_status_of_not_checked_properties(
   propertiest &properties,
   std::unordered_set<irep_idt> &updated_properties);
 
+/// Sets the property status of UNKNOWN properties to PASS.
+/// \param [in,out] properties: The status is updated in this data structure
+/// \param [in,out] updated_properties: The set of property IDs of
+///   updated properties
+/// Note: we currently declare everything PASS that is UNKNOWN at the
+///   end of the model checking algorithm.
+void update_status_of_unknown_properties(
+  propertiest &properties,
+  std::unordered_set<irep_idt> &updated_properties);
+
 // clang-format off
 #define OPT_BMC \
   "(program-only)" \