New goto-analyzer infrastructure : take 2

regression/goto-analyzer/Makefile

@@ -12,3 +12,9 @@ show:
 			vim -o "$$dir/*.java" "$$dir/*.out"; \
 		fi; \
 	done;
+
+clean:
+	find . -name *.*~ | xargs rm -f
+	find . -name *.out | xargs rm -f
+	find . -name *.goto | xargs rm -f
+	rm -f tests.log	

regression/goto-analyzer/constant_propagation_01/constant_propagation1.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i, j=20;
+
+  if (j==20)
+  {
+    int x=1,y=2,z;
+    z=x+y;
+    assert(z==3);
+  }
+
+}

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation1.c
+--constants --simplify out.goto
+^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$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i==0) 
+  {
+    i++;
+    j++;
+  }
+  assert(j!=3);
+}

regression/goto-analyzer/constant_propagation_02/original

@@ -0,0 +1,3 @@
+Task defaults to --show
+Domain defaults to --constants
+GOTO-ANALYSER version 5.5 64-bit x86_64 linux

regression/goto-analyzer/constant_propagation_02/simplified

@@ -0,0 +1,81 @@
+Reading GOTO program from `out.goto'
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+main /* main */
+        // 0 file constant_propagation_02.c line 5 function main
+        signed int i;
+        // 1 file constant_propagation_02.c line 5 function main
+        i = 0;
+        // 2 file constant_propagation_02.c line 5 function main
+        signed int j;
+        // 3 file constant_propagation_02.c line 5 function main
+        j = 2;
+        // 4 file constant_propagation_02.c line 7 function main
+        IF FALSE THEN GOTO 1
+        // 5 file constant_propagation_02.c line 9 function main
+        0 = 1;
+        // 6 file constant_propagation_02.c line 10 function main
+        2 = 3;
+        // 7 no location
+     1: SKIP
+        // 8 file constant_propagation_02.c line 12 function main
+        ASSERT FALSE // assertion j!=3
+        // 9 file constant_propagation_02.c line 12 function main
+        GOTO 2
+        // 10 file constant_propagation_02.c line 12 function main
+        (void)0;
+        // 11 no location
+     2: SKIP
+        // 12 file constant_propagation_02.c line 13 function main
+        dead j;
+        // 13 file constant_propagation_02.c line 13 function main
+        dead i;
+        // 14 file constant_propagation_02.c line 13 function main
+        main#return_value = NONDET(signed int);
+        // 15 file constant_propagation_02.c line 13 function main
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+_start /* _start */
+        // 16 no location
+        __CPROVER_initialize();
+        // 17 file constant_propagation_02.c line 3
+        main();
+        // 18 file constant_propagation_02.c line 3
+        return' = main#return_value;
+        // 19 file constant_propagation_02.c line 3
+        dead main#return_value;
+        // 20 file constant_propagation_02.c line 3
+        OUTPUT("return", return');
+        // 21 no location
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+__CPROVER_initialize /* __CPROVER_initialize */
+        // 22 no location
+        // Labels: __CPROVER_HIDE
+        SKIP
+        // 23 file <built-in-additions> line 39
+        __CPROVER_dead_object = NULL;
+        // 24 file <built-in-additions> line 38
+        __CPROVER_deallocated = NULL;
+        // 25 file <built-in-additions> line 42
+        __CPROVER_malloc_is_new_array = FALSE;
+        // 26 file <built-in-additions> line 40
+        __CPROVER_malloc_object = NULL;
+        // 27 file <built-in-additions> line 41
+        __CPROVER_malloc_size = 0ul;
+        // 28 file <built-in-additions> line 43
+        __CPROVER_memory_leak = NULL;
+        // 29 file <built-in-additions> line 31
+        __CPROVER_next_thread_id = 0ul;
+        // 30 file <built-in-additions> line 85
+        __CPROVER_pipe_count = 0u;
+        // 31 file <built-in-additions> line 65
+        __CPROVER_rounding_mode = 0;
+        // 32 file <built-in-additions> line 29
+        __CPROVER_thread_id = 0ul;
+        // 33 file <built-in-additions> line 30
+        __CPROVER_threads_exited = ARRAY_OF(FALSE);
+        // 34 no location
+        END_FUNCTION

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_02.c
+--constants --simplify out.goto
+^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$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i==0) 
+  {
+    i++;
+    j++;
+  }
+  assert(j==3);
+}

regression/goto-analyzer/constant_propagation_03/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_03.c
+--constants --simplify out.goto
+^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$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j==3);
+}

regression/goto-analyzer/constant_propagation_04/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_04.c
+--constants --simplify out.goto
+^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$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j!=3);
+}

regression/goto-analyzer/constant_propagation_05/test.desc

@@ -0,0 +1,8 @@
+CORE
+constant_propagation_05.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)$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+int main()
+{
+  int i, j=20;
+
+  if(i>=20)
+    assert(i>=10); // success
+
+  if(i>=10 && i<=20)
+    assert(i!=30); // success
+
+  if(i>=10 && i<=20)
+    assert(i!=15); // fails
+
+  if(i<1 && i>10)
+    assert(0); // success
+
+  if(i>=10 && j>=i)
+    assert(j>=10); // success
+
+  if(i>=j)
+    assert(i>=j); // unknown
+
+  if(i>10)
+    assert(i>=11); // success
+
+  if(i<=100 && j<i)
+    assert(j<100); // success
+}

regression/goto-analyzer/constant_propagation_06/test.desc

@@ -0,0 +1,15 @@
+CORE
+constant_propagation_06.c
+--intervals --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$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(i<51);
+}
+

regression/goto-analyzer/constant_propagation_07/test.desc

@@ -0,0 +1,8 @@
+CORE
+constant_propagation_07.c
+--constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<=50) 
+  {
+    i++;
+    j++;
+  }
+  assert(i<50);
+  assert(i<51);
+  assert(i<52);
+}
+

regression/goto-analyzer/constant_propagation_08/test.desc

@@ -0,0 +1,10 @@
+FUTURE
+constant_propagation_08.c
+--intervals --verify
+^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$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<=50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j<52);
+}
+

regression/goto-analyzer/constant_propagation_09/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_09.c
+--intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+******** Function main
+^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+int main()
+{
+  signed int i;
+  signed int j;
+  i = 0;
+   if(!(i >= 2))
+  {
+    j = j + 1;
+    i = i + 1;
+    if(!(i >= 2))
+    {
+      j = j + 1;
+      i = i + 1;
+      if(!(i >= 2))
+      {
+        j = j + 1;
+        i = i + 1;
+      }
+      assert(!(i < 2));
+    }
+  }
+  return 0;
+}
+

regression/goto-analyzer/constant_propagation_10/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_10.c
+--constants --simplify out.goto
+^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$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+int main()
+{
+  int a[2];
+  int i;
+  i = 0;
+
+  if (i==0)
+    a[0]=1;
+  else
+    a[1]=2;
+
+  assert(a[0]==1 || a[1]==2);
+
+  return 0;
+}
+