Merge pull request #2132 from tautschnig/extend-simplifier

Improvements to goto-analyzer's constant propagator and simplifier [blocks: #2522]

Author: tautschnig

regression/goto-analyzer/constant_propagation_03/test.desc

@@ -1,9 +1,9 @@
-FUTURE
+CORE
 main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
+^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_04/test.desc

@@ -1,9 +1,9 @@
-FUTURE
+CORE
 main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
+^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_05/test.desc

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

regression/goto-analyzer/constant_propagation_07/test.desc

@@ -1,9 +1,9 @@
-FUTURE
+CORE
 main.c
 --constants --simplify out.gb
 ^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$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 11, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_09/test.desc

@@ -1,9 +1,8 @@
-FUTURE
+CORE
 main.c
---constants --simplify out.gb
+--constants --verify
 ^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$
+^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 0: FAILURE \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_10/test.desc

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

regression/goto-analyzer/constant_propagation_11/test.desc

@@ -1,9 +1,8 @@
-FUTURE
+CORE
 main.c
---constants --simplify out.gb
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 0, assigns: 0, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 0, function calls: 0$
+^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 1: SUCCESS$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_12/test.desc

@@ -1,9 +1,9 @@
-FUTURE
+CORE
 main.c
 --constants --simplify out.gb
 ^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$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_13/test.desc

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

regression/goto-analyzer/constant_propagation_14/test.desc

@@ -1,9 +1,9 @@
-FUTURE
+CORE
 main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 11 function main, assertion tmp_if_expr: SUCCESS$
-^\[main.assertion.2\] file main.c line 12 function main, assertion tmp_if_expr\$1: FAILURE$
+^\[main.assertion.1\] line 11 assertion tmp_if_expr: SUCCESS$
+^\[main.assertion.2\] line 12 assertion tmp_if_expr\$0: FAILURE \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_15/test.desc

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

regression/goto-analyzer/constant_propagation_18/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  int i = 1;
+  int *p = &i;
+  assert(*p == 1);
+}

regression/goto-analyzer/constant_propagation_18/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line 7 assertion \*p == 1: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_19/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main()
+{
+  int x;
+  int *p = &x;
+  *p = 42;
+  assert(x == 42);
+  return 0;
+}

regression/goto-analyzer/constant_propagation_19/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line 8 assertion x == 42: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_two_way_1/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  int x;
+  if(x == 0)
+  {
+    assert(!x);
+  }
+  return 0;
+}

regression/goto-analyzer/constant_propagation_two_way_1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line 8 assertion !x: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/sensitivity-function-call-recursive/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+FUTURE
 main.c
 --variable --pointers --arrays --structs --verify
 ^EXIT=0$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+FUTURE
 sensitivity_test_constants_pointer_to_constants_struct.c
 --variable --pointers --structs --verify
 ^EXIT=0$