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

@@ -149,3 +149,89 @@ bool has_properties_to_check(const propertiest &properties)
   }
   return false;
 }
+
+/// Update with the preference order
+/// 1. old non-UNKNOWN/non-NOT_REACHED result
+/// 2. new non-UNKNOWN/non-NOT_REACHED result
+/// 3. UNKNOWN
+/// 4. NOT_REACHED
+/// Suitable for updating property results
+property_resultt &operator|=(property_resultt &a, property_resultt const &b)
+{
+  // non-monotonic use is likely a bug
+  PRECONDITION(
+    a == property_resultt::NOT_REACHED ||
+    (a == property_resultt::UNKNOWN && b != property_resultt::NOT_REACHED) ||
+    a == b);
+  switch(a)
+  {
+    case property_resultt::NOT_REACHED:
+    case property_resultt::UNKNOWN:
+      a = b;
+      return a;
+    case property_resultt::ERROR:
+    case property_resultt::PASS:
+    case property_resultt::NOT_REACHABLE:
+    case property_resultt::FAIL:
+      return a;
+  }
+  UNREACHABLE;
+}
+
+/// Update with the preference order
+/// 1. ERROR
+/// 2. FAIL
+/// 3. UNKNOWN
+/// 4. NOT_REACHED
+/// 5. NOT_REACHABLE
+/// 6. PASS
+/// Suitable for computing overall results
+property_resultt &operator&=(property_resultt &a, property_resultt const &b)
+{
+  switch(a)
+  {
+    case property_resultt::ERROR:
+      a = b;
+      return a;
+    case property_resultt::FAIL:
+      a = (b == property_resultt::ERROR ? b : a);
+      return a;
+    case property_resultt::UNKNOWN:
+      a = (b == property_resultt::ERROR || b == property_resultt::FAIL ? b : a);
+      return a;
+    case property_resultt::NOT_REACHED:
+      a = (b != property_resultt::PASS && b != property_resultt::NOT_REACHABLE? b : a);
+      return a;
+    case property_resultt::NOT_REACHABLE:
+      a = (b != property_resultt::PASS ? b : a);
+      return a;
+    case property_resultt::PASS:
+      a = (b == property_resultt::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_REACHED,
+///         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_resultt result = property_resultt::PASS;
+  for(const auto &property_pair : properties)
+  {
+    result &= property_pair.second.result;
+  }
+  // If we haven't reached anything or nothing is reachable
+  // then overall it's still a PASS.
+  if(
+    result == property_resultt::NOT_REACHED ||
+    result == property_resultt::NOT_REACHABLE)
+  {
+    result = property_resultt::PASS;
+  }
+  return static_cast<resultt>(result);
+}

src/goto-checker/properties.h

@@ -86,4 +86,8 @@ count_properties(const propertiest &properties, property_resultt result);
 
 bool has_properties_to_check(const propertiest &properties);
 
+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