Add a test case for per-history verification

This shows that call-stack sensitivity (unsurprisingly) can
significantly improve results -- but only with the previous patch.

Author: martin

regression/goto-analyzer/context_sensitivity_05/main.c

@@ -0,0 +1,54 @@
+#include <assert.h>
+
+void f00(int x, int y)
+{
+  if(x < 0)
+  {
+    // Unreachable in all traces if they are considered individually
+    assert(x < 0);
+    assert(1);
+    assert(0);
+  }
+
+  assert(x >= 0); // True in all traces
+  assert(x < 0);  // False in all traces
+  assert(x < 2);  // Split; true in some, false in others
+
+  assert((x <= 0) ? 1 : y);                  // True in some, unknown in others
+  assert((x <= 1) ? 0 : y);                  // False in some, unknown in others
+  assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
+
+  if(x < 5)
+  {
+    // Not reachable in all traces
+    assert((x <= 0) ? 1 : y); // True in some, unknown in others
+    assert((x <= 1) ? 0 : y); // False in some, unknown in others
+    assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
+  }
+
+  if(x < 3)
+  {
+    // Not reachable in all traces
+    assert((x <= 0) ? 1 : y); // True in some, unknown in others
+    assert((x <= 1) ? 0 : y); // False in some, unknown in others
+    assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
+  }
+}
+
+int nondet_int();
+
+int main(int argc, char **argv)
+{
+  int y = nondet_int();
+
+  // Because the history is context sensitive these should be analysed independently
+  // Just showing the domain will merge them giving top for everything interesting
+  f00(0, y);
+  f00(1, y);
+  f00(2, y);
+  f00(3, y);
+  f00(4, y);
+  f00(5, y);
+
+  return 0;
+}

regression/goto-analyzer/context_sensitivity_05/test.desc

@@ -0,0 +1,25 @@
+CORE
+main.c
+--verify --recursive-interprocedural --call-stack 0 --constants --one-domain-per-history
+^\[f00.assertion.1\] .* assertion x < 0: SUCCESS \(unreachable\)$
+^\[f00.assertion.2\] .* assertion 1: SUCCESS \(unreachable\)$
+^\[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.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$
+^\[f00.assertion.10\] .* assertion \(x <= 0\) \? 1 : y: UNKNOWN$
+^\[f00.assertion.11\] .* assertion \(x <= 1\) \? 0 : y: UNKNOWN$
+^\[f00.assertion.12\] .* assertion \(x <= 2\) \? \(\(x <= 3\) \? 1 : 0\) : y: UNKNOWN$
+^\[f00.assertion.13\] .* assertion \(x <= 0\) \? 1 : y: UNKNOWN$
+^\[f00.assertion.14\] .* assertion \(x <= 1\) \? 0 : y: UNKNOWN$
+^\[f00.assertion.15\] .* assertion \(x <= 2\) \? \(\(x <= 3\) \? 1 : 0\) : y: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests the verify tasks handling of multiple traces for each assertion
+