--vsd-flow-insensitive regression tests

Author: jezhiggins

regression/goto-analyzer/flow-insensitive-function-call-recursive/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+int fun(int other)
+{
+  if(other > 0)
+  {
+    int value = fun(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int main(int argc, char *argv[])
+{
+  int z = fun(0);
+  assert(z == 0); // Unknown as flow-insensitive fails to stop the recursive case being explored
+}

regression/goto-analyzer/flow-insensitive-function-call-recursive/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-flow-insensitive --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion z == 0: UNKNOWN$
+--
+^warning: ignoring

regression/goto-analyzer/flow-insensitive-if/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int y = 1;
+  int z;
+  if(y)
+  {
+    assert(y != 0);
+    z = 1;
+  }
+  else
+  {
+    assert(y == 0);
+    z = 0;
+  }
+  assert(z == 1);
+}

regression/goto-analyzer/flow-insensitive-if/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-flow-insensitive --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion y != 0: SUCCESS$
+^\[main\.assertion\.2\] .* assertion y == 0: FAILURE \(if reachable\)$
+^\[main\.assertion\.3\] .* assertion z == 1: UNKNOWN$
+--
+^warning: ignoring

regression/goto-analyzer/flow-sensitive-function-call-recursive/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+int fun(int other)
+{
+  if(other > 0)
+  {
+    int value = fun(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int main(int argc, char *argv[])
+{
+  int z = fun(0);
+  assert(z == 0); // Success because flow-sensitivity blocks the branch
+}

regression/goto-analyzer/flow-sensitive-function-call-recursive/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion z == 0: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/flow-sensitive-if/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int y = 1;
+  int z;
+  if(y)
+  {
+    assert(y != 0);
+    z = 1;
+  }
+  else
+  {
+    assert(y == 0);
+    z = 0;
+  }
+  assert(z == 1);
+}

regression/goto-analyzer/flow-sensitive-if/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion y != 0: SUCCESS$
+^\[main\.assertion\.2\] .* assertion y == 0: SUCCESS \(unreachable\)$
+^\[main\.assertion\.3\] .* assertion z == 1: SUCCESS$
+--
+^warning: ignoring