[path explore 3/7] Logical ops for resultt

The operators &= and |= can now be used between two
safety_checkert::resultt objects. They return the "best" or "worst" of
two results, and additionally assign that result to the LHS.  The
assignment operators are useful when repeatedly performing a safety
check and wanting to return a single error code that either describes
the best or worst outcome of all the safety checks combined.

Author: karkhaz

src/goto-programs/safety_checker.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 // this is just an interface -- it won't actually do any checking!
 
+#include <util/invariant.h>
 #include <util/message.h>
 
 #include "goto_trace.h"
@@ -45,4 +46,39 @@ class safety_checkert:public messaget
   const namespacet &ns;
 };
 
+/// \brief The worst of two results
+inline safety_checkert::resultt &
+operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
+{
+  switch(a)
+  {
+  case safety_checkert::resultt::ERROR:
+    return a;
+  case safety_checkert::resultt::SAFE:
+    a = b;
+    return a;
+  case safety_checkert::resultt::UNSAFE:
+    a = b == safety_checkert::resultt::ERROR ? b : a;
+    return a;
+  }
+  UNREACHABLE;
+}
+
+/// \brief The best of two results
+inline safety_checkert::resultt &
+operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
+{
+  switch(a)
+  {
+  case safety_checkert::resultt::SAFE:
+    return a;
+  case safety_checkert::resultt::ERROR:
+    a = b;
+    return a;
+  case safety_checkert::resultt::UNSAFE:
+    a = b == safety_checkert::resultt::SAFE ? b : a;
+    return a;
+  }
+  UNREACHABLE;
+}
 #endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H