Merge pull request #3570 from smowton/smowton/fix/value-set-member-type-safety

Fix value-set make_member function

Author: smowton

regression/cbmc/Linking7/member-name-mismatch.desc

@@ -1,11 +1,11 @@
-KNOWNBUG
+CORE
 main.c
 module2.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.c == 41: FAILURE
 ^\*\* 1 of 2 failed
 --
 ^warning: ignoring
---
-This is either a bug in goto-symex or value_sett (where the invariant fails).

regression/cbmc/Linking7/test.desc

@@ -5,5 +5,7 @@ module.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 ^\*\* 1 of 2 failed
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.b == 41: FAILURE
 --
 ^warning: ignoring

scripts/delete_failing_smt2_solver_tests

@@ -36,6 +36,7 @@ rm Float6/test.desc
 rm Float8/test.desc
 rm Linking4/test.desc
 rm Linking7/test.desc
+rm Linking7/member-name-mismatch.desc
 rm Malloc19/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc

src/pointer-analysis/value_set.cpp

@@ -1630,37 +1630,10 @@ exprt value_sett::make_member(
   const struct_union_typet &struct_union_type=
     to_struct_union_type(ns.follow(src.type()));
 
-  if(src.id()==ID_struct ||
-     src.id()==ID_constant)
-  {
-    std::size_t no=struct_union_type.component_number(component_name);
-    assert(no<src.operands().size());
-    return src.operands()[no];
-  }
-  else if(src.id()==ID_with)
-  {
-    assert(src.operands().size()==3);
-
-    // see if op1 is the member we want
-    const exprt &member_operand=src.op1();
-
-    if(component_name==member_operand.get(ID_component_name))
-      // yes! just take op2
-      return src.op2();
-    else
-      // no! do this recursively
-      return make_member(src.op0(), component_name, ns);
-  }
-  else if(src.id()==ID_typecast)
-  {
-    // push through typecast
-    assert(src.operands().size()==1);
-    return make_member(src.op0(), component_name, ns);
-  }
-
-  // give up
   const typet &subtype = struct_union_type.component_type(component_name);
-  member_exprt member_expr(src, component_name, subtype);
+  exprt member_expr = member_exprt(src, component_name, subtype);
+
+  simplify(member_expr, ns);
 
-  return std::move(member_expr);
+  return member_expr;
 }

src/util/pointer_offset_size.cpp

@@ -655,6 +655,13 @@ exprt get_subexpression_at_offset(
     return result;
   }
 
+  if(
+    offset_bytes == 0 && expr.type().id() == ID_pointer &&
+    target_type_raw.id() == ID_pointer)
+  {
+    return typecast_exprt(expr, target_type_raw);
+  }
+
   const typet &source_type = ns.follow(expr.type());
   const auto target_size_bits = pointer_offset_bits(target_type_raw, ns);
   if(!target_size_bits.has_value())