Merge pull request #2736 from diffblue/value_set_fi_hacks

tolerate two cases of imprecision in value_set_fi; addresses issue #2653

Author: tautschnig

src/pointer-analysis/value_set.cpp

@@ -1279,13 +1279,18 @@ void value_sett::assign(
           "rhs.type():\n" +
             rhs.type().pretty() + "\n" + "lhs.type():\n" + lhs.type().pretty());
 
-        const struct_typet &rhs_struct_type =
-          to_struct_type(ns.follow(rhs.type()));
+        const typet &followed = ns.follow(rhs.type());
 
-        const typet &rhs_subtype = rhs_struct_type.component_type(name);
-        rhs_member = simplify_expr(member_exprt{rhs, name, rhs_subtype}, ns);
+        if(followed.id() == ID_struct || followed.id() == ID_union)
+        {
+          const struct_union_typet &rhs_struct_union_type =
+            to_struct_union_type(followed);
+
+          const typet &rhs_subtype = rhs_struct_union_type.component_type(name);
+          rhs_member = simplify_expr(member_exprt{rhs, name, rhs_subtype}, ns);
 
-        assign(lhs_member, rhs_member, ns, true, add_to_sets);
+          assign(lhs_member, rhs_member, ns, true, add_to_sets);
+        }
       }
     }
   }

src/pointer-analysis/value_set_fi.cpp

@@ -411,17 +411,18 @@ void value_set_fit::get_value_set_rec(
   {
     const typet &type = to_index_expr(expr).array().type();
 
-    DATA_INVARIANT(type.id()==ID_array ||
-                   type.id()=="#REF#",
-                   "operand 0 of index expression must be an array");
-
-    get_value_set_rec(
-      to_index_expr(expr).array(),
-      dest,
-      "[]" + suffix,
-      original_type,
-      ns,
-      recursion_set);
+    if(type.id() == ID_array)
+    {
+      get_value_set_rec(
+        to_index_expr(expr).array(),
+        dest,
+        "[]" + suffix,
+        original_type,
+        ns,
+        recursion_set);
+    }
+    else
+      insert(dest, exprt(ID_unknown, original_type));
 
     return;
   }
@@ -1192,12 +1193,15 @@ void value_set_fit::assign_rec(
   {
     const typet &type = to_index_expr(lhs).array().type();
 
-    DATA_INVARIANT(type.id()==ID_array ||
-                   type.id()=="#REF#",
-                   "operand 0 of index expression must be an array");
-
-    assign_rec(
-      to_index_expr(lhs).array(), values_rhs, "[]" + suffix, ns, recursion_set);
+    if(type.id() == ID_array)
+    {
+      assign_rec(
+        to_index_expr(lhs).array(),
+        values_rhs,
+        "[]" + suffix,
+        ns,
+        recursion_set);
+    }
   }
   else if(lhs.id()==ID_member)
   {
@@ -1239,9 +1243,9 @@ void value_set_fit::assign_rec(
 
     assign_rec(typecast_expr.op(), values_rhs, suffix, ns, recursion_set);
   }
-  else if(lhs.id()=="zero_string" ||
-          lhs.id()=="is_zero_string" ||
-          lhs.id()=="zero_string_length")
+  else if(
+    lhs.id() == "zero_string" || lhs.id() == "is_zero_string" ||
+    lhs.id() == "zero_string_length" || lhs.id() == ID_address_of)
   {
     // ignore
   }