Tests for call stack history in the abstract interpreter

The existing --constants domain has some in-built handling of
recursion by proactively merging things which means that some of
these do not quite work.  Which is annoying.

Author: martin

regression/goto-analyzer/context_sensitivity_01/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+unsigned fib(unsigned x)
+{
+  switch(x)
+  {
+  case 0:
+    return 0;
+    break;
+  case 1:
+    return 1;
+    break;
+  default:
+    return fib(x - 1) + fib(x - 2);
+    break;
+  }
+}
+
+int main(int argc, char **argv)
+{
+  unsigned v = fib(7);
+  assert(v == 13); // Requires context sensitivity to handle with constants
+
+  unsigned w = fib(9);
+  assert(w == 24); // Requires location, not just function tracking
+
+  return 0;
+}

regression/goto-analyzer/context_sensitivity_01/test.desc

@@ -0,0 +1,12 @@
+FUTURE
+main.c
+--verify --recursive-interprocedural --call-stack 10 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion v == 13: SUCCESS$
+^\[main.assertion.2\] .* assertion w == 24: SUCCESS$
+--
+^warning: ignoring
+--
+This should be possible just tracking constants and calling stacks.
+At the moment the --constants domain can't do it due to the way it proactively merges to handle recursion.

regression/goto-analyzer/context_sensitivity_02/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int negate(int x)
+{
+  return -x;
+}
+
+int main(int argc, char **argv)
+{
+  int x = 23;
+  int nx = negate(x);
+  int nnx = negate(nx);
+
+  assert(x == nnx);
+
+  return 0;
+}

regression/goto-analyzer/context_sensitivity_02/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--verify --recursive-interprocedural --call-stack 0 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion x == nnx: SUCCESS$
+--
+^warning: ignoring
+--
+A simple test of call stacks and context sensitivity.  Merging calling context with contexts will give a failure.

regression/goto-analyzer/context_sensitivity_03/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int step(int x)
+{
+  if(x <= 0)
+  {
+    return 0;
+  }
+  else
+  {
+    return x + step(x - 1);
+  }
+}
+
+int main(int argc, char **argv)
+{
+  int x = 5;
+  int res = step(x);
+
+  assert(res == 15);
+
+  return 0;
+}

regression/goto-analyzer/context_sensitivity_03/test.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--verify --recursive-interprocedural --call-stack 10 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion res == 15: SUCCESS$
+--
+^warning: ignoring
+--
+This should be possible just tracking constants and calling stacks.
+At the moment the --constants domain can't do it due to the way it proactively merges to handle recursion.

regression/goto-analyzer/context_sensitivity_04/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int step(int x)
+{
+  if(x == 0)
+  {
+    assert(x == 0);
+    return 0;
+  }
+  else
+  {
+    return step(x - 1);
+  }
+}
+
+int main(int argc, char **argv)
+{
+  int orig = 20;
+  int res = step(orig);
+
+  assert(res == 0);
+
+  return 0;
+}

regression/goto-analyzer/context_sensitivity_04/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--verify --recursive-interprocedural --call-stack 10 --constants --one-domain-per-history
+^\[main.assertion.1\] .* assertion res == 0: SUCCESS$
+^\[step.assertion.1\] .* assertion x == 0: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests the interaction of call stacks and recursion.
+