Goto analyzer 6 part3

regression/goto-analyzer/constant_propagation_01/constant_propagation1.c → regression/goto-analyzer/constant_propagation_01/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -1,9 +1,9 @@
-FUTURE
-constant_propagation1.c
---constants --simplify out.goto
+CORE
+main.c
+--constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c → regression/goto-analyzer/constant_propagation_02/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -1,9 +1,9 @@
-FUTURE
-constant_propagation_02.c
---constants --simplify out.goto
+CORE
+main.c
+--constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c → regression/goto-analyzer/constant_propagation_03/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_03/test.desc

@@ -1,9 +1,9 @@
 FUTURE
-constant_propagation_03.c
---constants --simplify out.goto
+main.c
+--constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c → regression/goto-analyzer/constant_propagation_04/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_04/test.desc

@@ -1,9 +1,9 @@
 FUTURE
-constant_propagation_04.c
---constants --simplify out.goto
+main.c
+--constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c → regression/goto-analyzer/constant_propagation_05/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_05/test.desc

@@ -1,8 +1,8 @@
 FUTURE
-constant_propagation_05.c
+main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE (if reachable)$
+^\[main.assertion.1\] file main.c line 12 function main, assertion j!=3: Failure (if reachable)$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_06/main.c

@@ -0,0 +1,13 @@
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(i<51);
+}
+

regression/goto-analyzer/constant_propagation_06/test.desc

@@ -1,15 +1,8 @@
-FUTURE
-constant_propagation_06.c
---intervals --verify
+CORE
+main.c
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$
-^\[main.assertion.2\] file constant_propagation_06.c line 11 function main, assertion i!=30: SUCCESS$
-^\[main.assertion.3\] file constant_propagation_06.c line 14 function main, assertion i!=15: UNKNOWN$
-^\[main.assertion.4\] file constant_propagation_06.c line 17 function main, assertion 0: SUCCESS$
-^\[main.assertion.5\] file constant_propagation_06.c line 20 function main, assertion j>=10: SUCCESS$
-^\[main.assertion.6\] file constant_propagation_06.c line 23 function main, assertion i>=j: UNKNOWN$
-^\[main.assertion.7\] file constant_propagation_06.c line 26 function main, assertion i>=11: SUCCESS$
-^\[main.assertion.8\] file constant_propagation_06.c line 29 function main, assertion j<100: SUCCESS$
+^\[main.assertion.1\] file main.c line 11 function main, assertion i\s*<\s*51: Unknown$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c → regression/goto-analyzer/constant_propagation_07/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   signed int i;

regression/goto-analyzer/constant_propagation_07/test.desc

@@ -1,8 +1,9 @@
 FUTURE
-constant_propagation_07.c
---constants --verify
+main.c
+--constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$
+^Simplified:  assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c → regression/goto-analyzer/constant_propagation_08/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2];

regression/goto-analyzer/constant_propagation_08/test.desc

@@ -1,10 +1,9 @@
 FUTURE
-constant_propagation_08.c
---intervals --verify
+main.c
+--constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$
-^\[main.assertion.2\] file constant_propagation_08.c line 13 function main, assertion i<51: UNKNOWN$
-^\[main.assertion.3\] file constant_propagation_08.c line 14 function main, assertion i<52: SUCCESS$
+^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c → regression/goto-analyzer/constant_propagation_09/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_09/test.desc

@@ -1,9 +1,9 @@
 FUTURE
-constant_propagation_09.c
---intervals --verify
+main.c
+--constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-******** Function main
-^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c → regression/goto-analyzer/constant_propagation_10/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_10/test.desc

@@ -1,9 +1,8 @@
 FUTURE
-constant_propagation_10.c
---constants --simplify out.goto
+main.c
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
+^\[main.assertion.1\] file main.c line 10 function main, assertion a\[0\]==2: Failure$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c → regression/goto-analyzer/constant_propagation_11/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_11/test.desc

@@ -1,9 +1,9 @@
 FUTURE
-constant_propagation_11.c
---constants --simplify out.goto
+main.c
+--constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 0$
+^Unmodified:     assert: 0, assume: 0, goto: 0$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c → regression/goto-analyzer/constant_propagation_12/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int i=0, y;

regression/goto-analyzer/constant_propagation_12/test.desc

@@ -1,9 +1,9 @@
 FUTURE
-constant_propagation_12.c
---constants --simplify out.goto
+main.c
+--constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c → regression/goto-analyzer/constant_propagation_13/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int i=0, y;

regression/goto-analyzer/constant_propagation_13/test.desc

@@ -1,8 +1,8 @@
 FUTURE
-constant_propagation_13.c
+main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$
+^\[main.assertion.1\] file main.c line 9 function main, assertion y==0: Failure (if reachable)$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c → regression/goto-analyzer/constant_propagation_14/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_14/test.desc

@@ -1,9 +1,9 @@
 FUTURE
-constant_propagation_14.c
---constants --simplify out.goto
+main.c
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+^\[main.assertion.1\] file main.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: Success$
+^\[main.assertion.2\] file main.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: Failure$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c → regression/goto-analyzer/constant_propagation_15/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_15/test.desc

@@ -1,9 +1,8 @@
 FUTURE
-constant_propagation_15.c
---constants --simplify out.goto
+main.c
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$
+^\[main.assertion.1\] file main.c line 9 function main, assertion a\[0\]==2: Failure$
 --
 ^warning: ignoring