diff --git a/regression/cbmc/union11/union_list.c b/regression/cbmc/union11/union_list.c new file mode 100644 index 00000000000..0844303da79 --- /dev/null +++ b/regression/cbmc/union11/union_list.c @@ -0,0 +1,35 @@ +#include + +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 +} diff --git a/regression/cbmc/union11/union_list.desc b/regression/cbmc/union11/union_list.desc new file mode 100644 index 00000000000..e4d3a427794 --- /dev/null +++ b/regression/cbmc/union11/union_list.desc @@ -0,0 +1,8 @@ +CORE +union_list.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 21546b2e0a8..8a69eb3f54f 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/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); } } } diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index ba308ac8ea6..02ab9558042 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/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) {