Object descriptor should skip typecasts

tautschnig · tautschnig · commit 46a10b47c76f · 2016-05-30T11:44:07.000Z
diff --git 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);
+  }
 }
 
 /*******************************************************************\

Original file line number	Diff line number	Diff line change
`@@ -154,6 +154,14 @@ static void build_object_descriptor_rec(`
`154`	`154`	`typecast_exprt(to_byte_extract_expr(expr).offset(),`
`155`	`155`	`index_type));`
`156`	`156`	`}`
	`157`	`+ else if(expr.id()==ID_typecast)`
	`158`	`+ {`
	`159`	`+ const typecast_exprt &tc=to_typecast_expr(expr);`
	`160`	`+`
	`161`	`+ dest.object()=tc.op();`
	`162`	`+`
	`163`	`+ build_object_descriptor_rec(ns, tc.op(), dest);`
	`164`	`+ }`
`157`	`165`	`}`
`158`	`166`
`159`	`167`	`/*******************************************************************\`