Test showing loop terminates using constants, intervals, or value-sets

Author: jezhiggins

regression/goto-analyzer/loop-termination-ne/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int p = 1;
+
+  for(int i = 0; i != 5; ++i)
+    p += p;
+}

regression/goto-analyzer/loop-termination-ne/test-constants.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::1::i .* TOP @ \[3, 6\]
+^main::1::p .* TOP @ \[1, 5\]
+--

regression/goto-analyzer/loop-termination-ne/test-intervals.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::1::i .* \[0, 5\] @ \[3, 6\]
+^main::1::p .* \[1, 20\] @ \[1, 5\]
+--

regression/goto-analyzer/loop-termination-ne/test-value-sets.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::1::i .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[3, 6\]
+^main::1::p .* @ \[1, 5\]
+--