Merge pull request #6286 from jezhiggins/branching-history-and-assumptions

Static Verifier: Status should be UNKNOWN when there are true and false reachable traces

Author: martin-cs

regression/goto-analyzer/branching_history_01/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int global;
+
+int main(void)
+{
+  int local;
+  unsigned int nondet;
+
+  local = 1;
+  global = 1;
+
+  if(nondet == 0)
+  {
+    local = 2;
+  }
+  if(nondet == 0)
+  {
+    global = 2;
+  }
+
+  assert(local == global);
+}

regression/goto-analyzer/branching_history_01/test-no-unwind.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --recursive-interprocedural --vsd  
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .* local == global: UNKNOWN
+--

regression/goto-analyzer/branching_history_01/test-unwind.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --recursive-interprocedural --vsd  --loop-unwind-and-branching 10
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .* local == global: UNKNOWN
+--

regression/goto-analyzer/context_sensitivity_05/test.desc

@@ -6,7 +6,7 @@ main.c
 ^\[f00.assertion.3\] .* assertion 0: SUCCESS \(unreachable\)$
 ^\[f00.assertion.4\] .* assertion x >= 0: SUCCESS$
 ^\[f00.assertion.5\] .* assertion x < 0: FAILURE \(if reachable\)$
-^\[f00.assertion.6\] .* assertion x < 2: FAILURE \(if reachable\)$
+^\[f00.assertion.6\] .* assertion x < 2: UNKNOWN$
 ^\[f00.assertion.7\] .* assertion \(x <= 0\) \? 1 : y: UNKNOWN$
 ^\[f00.assertion.8\] .* assertion \(x <= 1\) \? 0 : y: UNKNOWN$
 ^\[f00.assertion.9\] .* assertion \(x <= 2\) \? \(\(x <= 3\) \? 1 : 0\) : y: UNKNOWN$

regression/goto-analyzer/local_control_flow_history_01/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* assertion x != 0: SUCCESS$
 ^\[main.assertion.2\] .* assertion x == 1: SUCCESS$
-^\[main.assertion.3\] .* assertion x == -1: FAILURE \(if reachable\)$
+^\[main.assertion.3\] .* assertion x == -1: UNKNOWN$
 ^\[main.assertion.4\] .* assertion x == 0: SUCCESS$
 --
 ^warning: ignoring

src/goto-analyzer/static_verifier.cpp

@@ -215,12 +215,8 @@ static_verifier_resultt::static_verifier_resultt(
           // The awkward case, there are traces that (may) reach it and
           // some are true, some are false.  It is not entirely fair to say
           // "FAILURE (if reachable)" because it's a bit more complex than
-          // that, "FAILURE (if reachable via a particular trace)" would be
-          // more accurate summary of what we know at this point.
-          // Given that all results of FAILURE from this analysis are
-          // caveated with some reachability questions, the following is not
-          // entirely unreasonable.
-          status = ai_verifier_statust::FALSE_IF_REACHABLE;
+          // that, and so the best we can say is UNKNOWN.
+          status = ai_verifier_statust::UNKNOWN;
         }
       }
     }
@@ -473,11 +469,9 @@ bool static_verifier(
     static_verifier_console(results, ns, m);
   }
 
-  m.status() << m.bold << "Summary: "
-             << pass << " pass, "
-             << fail << " fail if reachable, "
-             << unknown << " unknown"
-             << m.reset << messaget::eom;
+  m.status() << m.bold << "Summary: " << pass << " pass, " << fail
+             << " fail if reachable, " << unknown << " unknown" << m.reset
+             << messaget::eom;
 
   return false;
 }