diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 4c7a0bc9e2f..c1b93c11b41 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/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); + } } } } diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index dd93280c2fa..2cffde02bfb 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -410,17 +410,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 }