better precision of value_set on unions

regression/cbmc/union11/union_list.c

@@ -0,0 +1,35 @@
+#include <assert.h>
+
+struct list_item
+{
+  // there could be more members here, this single one suffices to demonstrate
+  // the problem/fix
+  struct list_item *previous;
+};
+
+struct List
+{
+  // an element such that the offset of "index" is non-zero
+  unsigned something;
+  struct list_item *index;
+  struct list_item end;
+};
+
+union U
+{
+  // there could be more members here, this single one suffices to demonstrate
+  // the problem/fix
+  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/union11/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

@@ -1204,7 +1204,7 @@ void value_sett::assign(
 
         rhs_member=make_member(rhs, name, ns);
 
-        assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
+        assign(lhs_member, rhs_member, ns, false, add_to_sets);
       }
     }
   }

src/util/simplify_expr_struct.cpp

@@ -172,6 +172,25 @@ bool simplify_exprt::simplify_member(exprt &expr)
 
       return false;
     }
+    else if(op_type.id() == ID_union)
+    {
+      // rewrite byte_extract(X, 0).member to X
+      // if the type of X is that of the member
+      const auto &byte_extract_expr = to_byte_extract_expr(op);
+      if(byte_extract_expr.offset().is_zero())
+      {
+        const union_typet &union_type = to_union_type(op_type);
+        const typet &subtype = union_type.component_type(component_name);
+
+        if(subtype == byte_extract_expr.op().type())
+        {
+          exprt tmp = byte_extract_expr.op();
+          expr.swap(tmp);
+
+          return false;
+        }
+      }
+    }
   }
   else if(op.id()==ID_union && op_type.id()==ID_union)
   {