Update and check the test cases. FUTURE for things where precision is currently insufficient.

martin · martin · commit a7be3a6d1bfd · 2016-11-01T11:06:21.000Z
diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -3,7 +3,7 @@ constant_propagation1.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 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
diff --git a/regression/goto-analyzer/constant_propagation_02/original b/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
diff --git a/regression/goto-analyzer/constant_propagation_02/simplified b/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
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -3,7 +3,7 @@ constant_propagation_02.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 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
diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc
@@ -3,7 +3,7 @@ constant_propagation_03.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 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
diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc
@@ -3,7 +3,7 @@ constant_propagation_04.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 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
diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc
@@ -3,6 +3,6 @@ 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$
+^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_06.c
---constants --intervals --verify
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$
diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc
@@ -3,7 +3,6 @@ constant_propagation_07.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<50: UNKNOWN$
-^\[main.assertion.2\] file constant_propagation_07.c line 13 function main, assertion i<51: SUCCESS$
+^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 constant_propagation_08.c
---constants --intervals --verify
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$
diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_09.c
---constants --intervals --verify
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ******** Function main
diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc
@@ -3,7 +3,7 @@ constant_propagation_10.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 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
diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc
@@ -1,9 +1,9 @@
-CORE
-constant_propagation_10.c
+FUTURE
+constant_propagation_11.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 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$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc
@@ -1,9 +1,9 @@
-CORE
+FUTURE
 constant_propagation_12.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 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$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 constant_propagation_13.c
 --constants --verify
 ^EXIT=0$
diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 constant_propagation_14.c
 --constants --simplify out.goto
 ^EXIT=0$
diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc
@@ -1,9 +1,9 @@
-CORE
+FUTURE
 constant_propagation_15.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 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$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_16/test.desc b/regression/goto-analyzer/constant_propagation_16/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 constant_propagation_16.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_16.c line 9 function main, assertion y==0: FAILURE$
+^\[main.assertion.1\] file constant_propagation_16.c line 9 function main, assertion y==0: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 constant_propagation_17.c
 --constants --verify
 ^EXIT=0$
diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 constant_propagation_18.c
 --constants --verify
 ^EXIT=0$
diff --git a/regression/goto-analyzer/intervals10/test.desc b/regression/goto-analyzer/intervals10/test.desc
@@ -1,12 +1,12 @@
-CORE
+FUTURE
 intervals10.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file intervals10.c line 8 function main, assertion j<=100: SUCCESS$
 ^\[main.assertion.2\] file intervals10.c line 11 function main, assertion j<101: SUCCESS$
-^\[main.assertion.3\] file intervals10.c line 14 function main, assertion j>100: UNKNOWN$
+^\[main.assertion.3\] file intervals10.c line 14 function main, assertion j>100: FAILURE (if reachable)$
 ^\[main.assertion.4\] file intervals10.c line 17 function main, assertion j<99: UNKNOWN$
-^\[main.assertion.5\] file intervals10.c line 20 function main, assertion j==100: UNKNOWN$
+^\[main.assertion.5\] file intervals10.c line 20 function main, assertion j==100: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals11/test.desc b/regression/goto-analyzer/intervals11/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 intervals11.c
 --intervals --verify
 ^EXIT=0$
diff --git a/regression/goto-analyzer/intervals12/intervals12.c b/regression/goto-analyzer/intervals12/intervals12.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main (void) {
+  int i;
+  int j;
+
+  if (i <= 0 && j < i)
+    assert(j < 0);
+
+  if (j < i && i <= 0)
+    assert(j < 0);
+
+  return 0;
+}
+
+
diff --git a/regression/goto-analyzer/intervals12/test.desc b/regression/goto-analyzer/intervals12/test.desc
@@ -0,0 +1,9 @@
+FUTURE
+intervals12.c
+--intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^[main.assertion.1] file intervals12.c line 8 function main, assertion j < 0: SUCCESS$
+^[main.assertion.2] file intervals12.c line 11 function main, assertion j < 0: SUCCESS$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/intervals6/test.desc b/regression/goto-analyzer/intervals6/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 intervals6.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: UNKNOWN$
+^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals7/test.desc b/regression/goto-analyzer/intervals7/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 intervals7.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: UNKNOWN$
+^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals8/test.desc b/regression/goto-analyzer/intervals8/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 intervals8.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file intervals8.c line 6 function main, assertion x < -10 && x < 100: UNKNOWN$
+^\[main.assertion.1\] file intervals8.c line 6 function main, assertion x < -10 && x < 100: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals9/intervals9.c b/regression/goto-analyzer/intervals9/intervals9.c
@@ -1,4 +1,4 @@
-//#include <assert.h>
+#include <assert.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/intervals9/test.desc b/regression/goto-analyzer/intervals9/test.desc
@@ -3,6 +3,6 @@ intervals9.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file intervals9.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$
+^\[main.assertion.1\] file intervals9.c line 9 function main, assertion i>=1 && i<=2: SUCCESS$
 --
 ^warning: ignoring

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+Task defaults to --show`
	`2`	`+Domain defaults to --constants`
	`3`	`+GOTO-ANALYSER version 5.5 64-bit x86_64 linux`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+FUTURE`
`2`	`2`	`constant_propagation_13.c`
`3`	`3`	`--constants --verify`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-//#include <assert.h>`
	`1`	`+#include <assert.h>`
`2`	`2`
`3`	`3`	`int main()`
`4`	`4`	`{`