Merge pull request #6541 from tautschnig/fix-rmc-708

Simplification of nested pointer arithmetic: do not assume same type

Author: kroening

regression/cbmc/Pointer_Arithmetic15/main.c

@@ -15,5 +15,9 @@ int main()
 
   a = p - q;
 
+  // mixing types: the C front-end will insert casts
+  unsigned long long u;
+  p = (p + a) + u;
+
   assert(0);
 }

src/util/simplify_expr_int.cpp

@@ -439,16 +439,24 @@ simplify_exprt::resultt<> simplify_exprt::simplify_plus(const plus_exprt &expr)
       expr.op0().id() == ID_plus && expr.op0().type().id() == ID_pointer &&
       expr.op0().operands().size() == 2)
     {
-      plus_exprt op0 = to_plus_expr(expr.op0());
+      plus_exprt result = to_plus_expr(expr.op0());
+      if(as_const(result).op0().type().id() != ID_pointer)
+        result.op0().swap(result.op1());
+      const exprt &op1 = as_const(result).op1();
 
-      if(op0.op1().id() == ID_plus)
-        to_plus_expr(op0.op1()).add_to_operands(expr.op1());
+      if(op1.id() == ID_plus)
+      {
+        plus_exprt new_op1 = to_plus_expr(op1);
+        new_op1.add_to_operands(
+          typecast_exprt::conditional_cast(expr.op1(), new_op1.op0().type()));
+        result.op1() = simplify_plus(new_op1);
+      }
       else
-        op0.op1()=plus_exprt(op0.op1(), expr.op1());
-
-      auto result = op0;
-
-      result.op1() = simplify_plus(to_plus_expr(result.op1()));
+      {
+        plus_exprt new_op1{
+          op1, typecast_exprt::conditional_cast(expr.op1(), op1.type())};
+        result.op1() = simplify_plus(new_op1);
+      }
 
       return changed(simplify_plus(result));
     }