better precision of value_set on unions

Author: Daniel Kroening

regression/cbmc/union10/union_list.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+struct list_item
+{
+  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 );
+  u.my_list.end.previous = u.my_list.index;
+  struct list_item *p1 = u.my_list.index;
+  struct list_item *p2 = p1->previous;
+  struct list_item *p3 = p2->previous;
+  assert(p3!=0); // should pass
+}

regression/cbmc/union10/union_list.desc

@@ -0,0 +1,8 @@
+CORE
+union_list.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/pointer-analysis/value_set.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/base_type.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
@@ -1755,9 +1756,23 @@ exprt value_sett::make_member(
     assert(src.operands().size()==1);
     return make_member(src.op0(), component_name, ns);
   }
+  else if(src.id()==ID_byte_extract_little_endian ||
+          src.id()==ID_byte_extract_big_endian)
+  {
+    const typet subtype=struct_union_type.component_type(component_name);
+    const auto &byte_extract_expr = to_byte_extract_expr(src);
+    if(struct_union_type.id()==ID_union &&
+       subtype==byte_extract_expr.op().type() &&
+       byte_extract_expr.offset().is_zero())
+    {
+      // rewrite byte_extract(X, 0).member to X
+      // if the type of X is that of the member
+      return byte_extract_expr.op();
+    }
+  }
 
   // give up
-  typet subtype=struct_union_type.component_type(component_name);
+  const typet subtype=struct_union_type.component_type(component_name);
   member_exprt member_expr(src, component_name, subtype);
 
   return member_expr;