From 46a10b47c76f9355029a4b939ea055e3d8a3c23c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 6 Mar 2016 18:50:10 +0000 Subject: [PATCH 1/2] Object descriptor should skip typecasts --- src/util/std_expr.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 42fb6f13201..08a1cf59760 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -154,6 +154,14 @@ static void build_object_descriptor_rec( typecast_exprt(to_byte_extract_expr(expr).offset(), index_type)); } + else if(expr.id()==ID_typecast) + { + const typecast_exprt &tc=to_typecast_expr(expr); + + dest.object()=tc.op(); + + build_object_descriptor_rec(ns, tc.op(), dest); + } } /*******************************************************************\ From 03c1b4127a8c7f277cf859f5a298a28ed65ec685 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Mar 2016 22:24:43 +0000 Subject: [PATCH 2/2] Do not require a constant member offset when building a byte-extract expression --- src/util/std_expr.cpp | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 08a1cf59760..25fbc97ad0f 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -125,20 +125,15 @@ static void build_object_descriptor_rec( { const member_exprt &member=to_member_expr(expr); const exprt &struct_op=member.struct_op(); - const typet &struct_type=ns.follow(struct_op.type()); build_object_descriptor_rec(ns, struct_op, dest); - if(struct_type.id()==ID_union) - return; - - mp_integer offset= - member_offset(to_struct_type(struct_type), - member.get_component_name(), ns); - assert(offset>=0); + exprt offset=member_offset_expr(member, ns); + assert(offset.is_not_nil()); dest.offset()= - plus_exprt(dest.offset(), from_integer(offset, index_type)); + plus_exprt(dest.offset(), + typecast_exprt(offset, index_type)); } else if(expr.id()==ID_byte_extract_little_endian || expr.id()==ID_byte_extract_big_endian)