Add functions to combine property results

Used to update the properties map and
to compute the overall result.

Author: peterschrammel

src/goto-checker/properties.cpp

@@ -143,3 +143,92 @@ count_properties(const propertiest &properties, property_statust status)
   }
   return count;
 }
+
+/// Update with the preference order
+/// 1. old non-UNKNOWN/non-NOT_CHECKED status
+/// 2. new non-UNKNOWN/non-NOT_CHECKED status
+/// 3. UNKNOWN
+/// 4. NOT_CHECKED
+/// Suitable for updating property status
+property_statust &operator|=(property_statust &a, property_statust const &b)
+{
+  // non-monotonic use is likely a bug
+  PRECONDITION(
+    a == property_statust::NOT_CHECKED ||
+    (a == property_statust::UNKNOWN && b != property_statust::NOT_CHECKED) ||
+    a == b);
+  switch(a)
+  {
+    case property_statust::NOT_CHECKED:
+    case property_statust::UNKNOWN:
+      a = b;
+      return a;
+    case property_statust::ERROR:
+    case property_statust::PASS:
+    case property_statust::NOT_REACHABLE:
+    case property_statust::FAIL:
+      return a;
+  }
+  UNREACHABLE;
+}
+
+/// Update with the preference order
+/// 1. ERROR
+/// 2. FAIL
+/// 3. UNKNOWN
+/// 4. NOT_CHECKED
+/// 5. NOT_REACHABLE
+/// 6. PASS
+/// Suitable for computing overall results
+property_statust &operator&=(property_statust &a, property_statust const &b)
+{
+  switch(a)
+  {
+    case property_statust::ERROR:
+      a = b;
+      return a;
+    case property_statust::FAIL:
+      a = (b == property_statust::ERROR ? b : a);
+      return a;
+    case property_statust::UNKNOWN:
+      a = (b == property_statust::ERROR || b == property_statust::FAIL ? b : a);
+      return a;
+    case property_statust::NOT_CHECKED:
+      a = (b != property_statust::PASS && b != property_statust::NOT_REACHABLE? b : a);
+      return a;
+    case property_statust::NOT_REACHABLE:
+      a = (b != property_statust::PASS ? b : a);
+      return a;
+    case property_statust::PASS:
+      a = (b == property_statust::PASS ? a : b);
+      return a;
+  }
+  UNREACHABLE;
+}
+
+/// Determines the overall result corresponding from the given properties
+/// That is PASS if all properties are PASS or NOT_CHECKED,
+///         FAIL if at least one property is FAIL and no property is ERROR,
+///         UNKNOWN if no property is FAIL or ERROR and
+///           at least one property is UNKNOWN,
+///         ERROR if at least one property is error.
+resultt determine_result(const propertiest &properties)
+{
+  property_statust result = property_statust::PASS;
+  for(const auto &property_pair : properties)
+  {
+    result &= property_pair.second.result;
+  }
+  // If we have unchecked properties then we don't know.
+  if(result == property_statust::NOT_CHECKED)
+  {
+    result = property_statust::UNKNOWN;
+  }
+  // If a property is not reachable,
+  // then overall it's still a PASS.
+  else if(result == property_statust::NOT_REACHABLE)
+  {
+    result = property_statust::PASS;
+  }
+  return static_cast<resultt>(result);
+}

src/goto-checker/properties.h

@@ -90,4 +90,8 @@ int result_to_exit_code(resultt result);
 std::size_t
 count_properties(const propertiest &, property_statust);
 
+property_resultt &operator|=(property_resultt &, property_resultt const &);
+property_resultt &operator&=(property_resultt &, property_resultt const &);
+resultt determine_result(const propertiest &properties);
+
 #endif // CPROVER_GOTO_CHECKER_PROPERTIES_H