Merge pull request #2854 from diffblue/union-valueset-bug

added a test for the precision of the value sets on unions

Author: tautschnig

regression/cbmc/union10/union_list2.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+
+struct list_item
+{
+  unsigned value;
+  struct list_item *previous;
+};
+
+struct List
+{
+  unsigned something;
+  struct list_item * index, end;
+};
+
+union U
+{
+  struct List my_list;
+};
+
+int main()
+{
+  union U u;
+
+  u.my_list.index = &u.my_list.end;
+  struct list_item *p0 = u.my_list.index;
+  u.my_list.end.value = 123;
+  u.my_list.end.previous = u.my_list.index;
+  struct list_item *p1 = u.my_list.index;
+  struct list_item *p2 = p1->previous;
+  assert(p2 != 0); // should pass
+}

regression/cbmc/union10/union_list2.desc

@@ -0,0 +1,18 @@
+KNOWNBUG
+union_list2.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Value sets do not record byte-extract operations with sufficient detail:
+  struct list_item *p1 = u.my_list.index;
+  struct list_item *p2 = p1->previous;
+yields
+  (29) p1!0@1#2 == byte_extract_little_endian(u!0@1#4, 8l, struct list_item { unsigned int value; unsigned int $pad1; struct list_item *previous; } *)
+  (30) p2!0@1#2 == p1$object#0.previous
+as
+  main::1::p1 = { <integer_address, *, unsigned char> }
+is the only information stored in the value set.