Merge pull request #7230 from tautschnig/feature/union-field-sensitivity

Field sensitivity for unions
diffblue · Nov 22, 2022 · f1aaf5b · f1aaf5b
2 parents e3ee9a9 + 50dbf7e
commit f1aaf5b
Show file tree

Hide file tree

Showing 16 changed files with 286 additions and 50 deletions.
diff --git a/regression/cbmc/Float22/test.desc b/regression/cbmc/Float22/test.desc
@@ -1,11 +1,8 @@
-CORE broken-cprover-smt-backend
+CORE
 main.c
 --floatbv
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
---
-Fixing this test for the CPROVER SMT2 solver (or any other SMT2 solver
-supporting FPA) requires addressing the TODO "bit-wise floatbv to bv".
diff --git a/regression/cbmc/Pointer_Arithmetic19/test.desc b/regression/cbmc/Pointer_Arithmetic19/test.desc
@@ -1,7 +1,6 @@
 CORE new-smt-backend
 main.c
 --program-only
-ASSERT\(byte_extract_little_endian\(\{ 42, 43 \}, POINTER_OFFSET\(p!0@1#2\), signed int\) == 43\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/cbmc/array-cell-sensitivity15/test.desc b/regression/cbmc/array-cell-sensitivity15/test.desc
@@ -3,7 +3,7 @@ access.c
 --program-only
 ^EXIT=0$
 ^SIGNAL=0$
-s!0@1#1\.\.n == \{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] } WITH \[\(.*\)i!0@1#2:=k!0@1#1\]
+s!0@1#2\.\.n == \{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] } WITH \[\(.*\)i!0@1#2:=k!0@1#1\]
 --
 byte_update
 --

diff --git a/regression/cbmc/array-cell-sensitivity8/test.desc b/regression/cbmc/array-cell-sensitivity8/test.desc
@@ -10,7 +10,7 @@ main::1::array!0@1#2\[\[6\]\] =
 main::1::array!0@1#2\[\[7\]\] =
 main::1::array!0@1#2\[\[8\]\] =
 main::1::array!0@1#2\[\[9\]\] =
-main::1::array!0@1#2 =.*byte_extract_little_endian
+main::1::array!0@1#3 =.*byte_extract_little_endian
 main::1::array!0@1#3\[\[0\]\] =
 main::1::array!0@1#3\[\[1\]\] =
 main::1::array!0@1#3\[\[2\]\] =

diff --git a/regression/cbmc/field-sensitivity9/test.desc b/regression/cbmc/field-sensitivity9/test.desc
@@ -1,8 +1,8 @@
 CORE
 test.c
 --show-vcc
-main::1::a1!0@1#1 =
-main::1::a2!0@1#1 =
+main::1::a1!0@1#2 =
+main::1::a2!0@1#2 =
 main::1::a1!0@1#2\.\.x =
 main::1::a1!0@1#2\.\.y =
 main::1::a1!0@1#2\.\.z =

diff --git a/regression/cbmc/gcc_vector1/test.desc b/regression/cbmc/gcc_vector1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/union/union_large_array.desc b/regression/cbmc/union/union_large_array.desc
@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend
+CORE thorough-smt-backend
 union_large_array.c
 
 ^EXIT=10$
@@ -9,3 +9,8 @@ union_large_array.c
 --
 ^warning: ignoring
 --
+Union field sensitivity yields an equation over the (large) array member, which
+results in one assertion per array element. The formula is generated in 150
+seconds, with a file size of 98 MB. Solving requires several GB of memory.
+Adding --slice-formula would avoid the problem, but would remove all interesting
+parts of this regression test.
diff --git a/regression/cbmc/union18/main.c b/regression/cbmc/union18/main.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+union u_type
+{
+  int i;
+  char ch;
+};
+
+int main()
+{
+  union u_type u;
+
+  u.ch = 2;
+  assert(u.ch == 2);
+}
diff --git a/regression/cbmc/union18/test.desc b/regression/cbmc/union18/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This should be fully solved by constant propagation when union field-sensitivity
+is in place.