Merge pull request #5703 from tautschnig/union-test-1

Additional and updated union regression tests involving pointers

Author: tautschnig

regression/cbmc/union10/union_list2.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 union_list2.c
 
 ^EXIT=0$

regression/cbmc/union14/main.c

@@ -0,0 +1,47 @@
+struct fatptr
+{
+  int *data;
+  unsigned long int len;
+};
+
+struct slice
+{
+  int *data;
+  unsigned long int len;
+};
+
+union repr {
+  struct slice rust;
+  struct fatptr raw;
+};
+
+struct slice cast(int *data, unsigned long int len)
+{
+  struct fatptr x;
+  union repr z;
+  x.data = data;
+  x.len = len;
+  z.raw = x;
+  return z.rust;
+}
+
+struct fatptr cast2(int *data, unsigned long int len)
+{
+  struct slice w;
+  union repr z;
+  w.data = data;
+  w.len = len;
+  z.rust = w;
+  return z.raw;
+}
+
+int main()
+{
+  int x = 256;
+
+  struct slice z = cast(&x, 1);
+  struct fatptr z2 = cast2(&x, 1);
+
+  __CPROVER_assert(*z.data == 256, "test 1");
+  __CPROVER_assert(*z2.data == 256, "test 2");
+}

regression/cbmc/union14/test.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Value sets do not properly track pointers through byte-extract operations. Thus
+derferencing yields __CPROVER_memory, which results in a spurious verification
+failure.