Merge pull request #6300 from jezhiggins/vsd-assertions-intervals-and-value-sets

VSD - Regression tests to capture behaviour of assertions

Author: martin-cs

regression/goto-analyzer/variable-sensitivity-asserts-01/main.c

@@ -0,0 +1,17 @@
+
+int main(void)
+{
+  int x = 1;
+  int y = 3;
+  int nondet;
+
+  if(nondet)
+    y = 5;
+  if(nondet)
+    x = 2;
+
+  __CPROVER_assert(x < y, "x < y");
+  __CPROVER_assert(x <= y, "x <= y");
+  __CPROVER_assert(y > x, "y > x");
+  __CPROVER_assert(y >= x, "y >= x");
+}

regression/goto-analyzer/variable-sensitivity-asserts-01/test-constants.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line 13 x < y: UNKNOWN
+\[main.assertion.2\] line 14 x <= y: UNKNOWN
+\[main.assertion.3\] line 15 y > x: UNKNOWN
+\[main.assertion.4\] line 16 y >= x: UNKNOWN
+--

regression/goto-analyzer/variable-sensitivity-asserts-01/test-intervals.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line 13 x < y: SUCCESS
+\[main.assertion.2\] line 14 x <= y: SUCCESS
+\[main.assertion.3\] line 15 y > x: SUCCESS
+\[main.assertion.4\] line 16 y >= x: SUCCESS
+--

regression/goto-analyzer/variable-sensitivity-asserts-01/test-value-sets.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line 13 x < y: SUCCESS
+\[main.assertion.2\] line 14 x <= y: SUCCESS
+\[main.assertion.3\] line 15 y > x: SUCCESS
+\[main.assertion.4\] line 16 y >= x: SUCCESS
+--

regression/goto-analyzer/variable-sensitivity-asserts-02/main.c

@@ -0,0 +1,21 @@
+
+int main(void)
+{
+  int x = 1;
+  int y = 3;
+  int nondet;
+
+  if(nondet)
+    y = 1;
+  if(nondet)
+    x = 3;
+
+  __CPROVER_assert(x == y, "x == y");
+  __CPROVER_assert(y == x, "y == x");
+  __CPROVER_assert(!(x == y), "!(x == y)");
+  __CPROVER_assert(!(y == x), "!(y == x)");
+  __CPROVER_assert(x != y, "x != y");
+  __CPROVER_assert(y != x, "y != x");
+  __CPROVER_assert(!(x != y), "!(x != y)");
+  __CPROVER_assert(!(y != x), "!(y != x)");
+}

regression/goto-analyzer/variable-sensitivity-asserts-02/test-constants.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line 13 x == y: UNKNOWN
+\[main.assertion.2\] line 14 y == x: UNKNOWN
+\[main.assertion.3\] line 15 !\(x == y\): UNKNOWN
+\[main.assertion.4\] line 16 !\(y == x\): UNKNOWN
+\[main.assertion.5\] line 17 x != y: UNKNOWN
+\[main.assertion.6\] line 18 y != x: UNKNOWN
+\[main.assertion.7\] line 19 !\(x != y\): UNKNOWN
+\[main.assertion.8\] line 20 !\(y != x\): UNKNOWN
+--

regression/goto-analyzer/variable-sensitivity-asserts-02/test-intervals.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line 13 x == y: SUCCESS
+\[main.assertion.2\] line 14 y == x: SUCCESS
+\[main.assertion.3\] line 15 !\(x == y\): FAILURE
+\[main.assertion.4\] line 16 !\(y == x\): FAILURE
+\[main.assertion.5\] line 17 x != y: FAILURE
+\[main.assertion.6\] line 18 y != x: FAILURE
+\[main.assertion.7\] line 19 !\(x != y\): SUCCESS
+\[main.assertion.8\] line 20 !\(y != x\): SUCCESS
+--

regression/goto-analyzer/variable-sensitivity-asserts-02/test-value-sets.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line 13 x == y: UNKNOWN
+\[main.assertion.2\] line 14 y == x: UNKNOWN
+\[main.assertion.3\] line 15 !\(x == y\): UNKNOWN
+\[main.assertion.4\] line 16 !\(y == x\): UNKNOWN
+\[main.assertion.5\] line 17 x != y: UNKNOWN
+\[main.assertion.6\] line 18 y != x: UNKNOWN
+\[main.assertion.7\] line 19 !\(x != y\): UNKNOWN
+\[main.assertion.8\] line 20 !\(y != x\): UNKNOWN
+--

regression/goto-analyzer/variable-sensitivity-asserts-03/main.c

@@ -0,0 +1,21 @@
+
+int main(void)
+{
+  int x = 1;
+  int y = 3;
+  int nondet;
+
+  if(nondet)
+    y = 1;
+  if(nondet)
+    x = 5;
+
+  __CPROVER_assert(x != y, "x != y");
+  __CPROVER_assert(y != x, "y != x");
+  __CPROVER_assert(!(x != y), "!(x != y)");
+  __CPROVER_assert(!(y != x), "!(y != x)");
+  __CPROVER_assert(x == y, "x == y");
+  __CPROVER_assert(y == x, "y == x");
+  __CPROVER_assert(!(x == y), "!(x == y)");
+  __CPROVER_assert(!(y == x), "!(y == x)");
+}

regression/goto-analyzer/variable-sensitivity-asserts-03/test-constants.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line 13 x != y: UNKNOWN
+\[main.assertion.2\] line 14 y != x: UNKNOWN
+\[main.assertion.3\] line 15 !\(x != y\): UNKNOWN
+\[main.assertion.4\] line 16 !\(y != x\): UNKNOWN
+\[main.assertion.5\] line 17 x == y: UNKNOWN
+\[main.assertion.6\] line 18 y == x: UNKNOWN
+\[main.assertion.7\] line 19 !\(x == y\): UNKNOWN
+\[main.assertion.8\] line 20 !\(y == x\): UNKNOWN
+--