@@ -318,12 +318,14 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
318318 // (int)((T*)0 + int) -> (int)(sizeof(T)*(size_t)int) if NULL is zero
319319 if (config.ansi_c .NULL_is_zero &&
320320 (expr_type.id ()==ID_signedbv || expr_type.id ()==ID_unsignedbv) &&
321+ op_type.id ()==ID_pointer &&
321322 expr.op0 ().id ()==ID_plus &&
322323 expr.op0 ().operands ().size ()==2 &&
323- expr.op0 ().op0 ().id ()==ID_typecast &&
324+ (( expr.op0 ().op0 ().id ()==ID_typecast &&
324325 expr.op0 ().op0 ().operands ().size ()==1 &&
325- expr.op0 ().op0 ().op0 ().is_zero () &&
326- op_type.id ()==ID_pointer)
326+ expr.op0 ().op0 ().op0 ().is_zero ()) ||
327+ (expr.op0 ().op0 ().is_constant () &&
328+ to_constant_expr (expr.op0 ().op0 ()).get_value ()==ID_NULL)))
327329 {
328330 mp_integer sub_size=pointer_offset_size (op_type.subtype (), ns);
329331 if (sub_size!=-1 )
@@ -727,6 +729,20 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
727729 return false ;
728730 }
729731 }
732+ else if (operand.id ()==ID_address_of)
733+ {
734+ const exprt &o=to_address_of_expr (operand).object ();
735+
736+ // turn &array into &array[0] when casting to pointer-to-element-type
737+ if (o.type ().id ()==ID_array &&
738+ base_type_eq (expr_type, pointer_type (o.type ().subtype ()), ns))
739+ {
740+ expr=address_of_exprt (index_exprt (o, from_integer (0 , size_type ())));
741+
742+ simplify_rec (expr);
743+ return false ;
744+ }
745+ }
730746
731747 return true ;
732748}
0 commit comments