Use pointer difference type when adding to pointer

tautschnig · tautschnig · commit 1fc3118ed70a · 2018-08-13T16:21:38.000Z
The back-end will support signed and unsigned addition to pointers, but mixing
signed/unsigned is not permitted. The previous code would generate such a mixed
expression when first goto_checkt and later address_arithmetic would add onto a
pointer.
diff --git a/regression/cbmc/member1/main.c b/regression/cbmc/member1/main.c
@@ -0,0 +1,19 @@
+struct B
+{
+  int bi;
+  int *c;
+};
+
+struct A
+{
+  int ai;
+  struct B b;
+};
+
+int main()
+{
+  struct A *a;
+  if((&a->b)->c == 0)
+    return 1;
+  return 0;
+}
diff --git a/regression/cbmc/member1/test.desc b/regression/cbmc/member1/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+add/sub with mixed types
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
@@ -1414,7 +1414,10 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
           deref.pointer(), pointer_type(char_type()));
 
       const exprt new_address = typecast_exprt(
-        plus_exprt(char_pointer, member_offset), char_pointer.type());
+        plus_exprt(
+          char_pointer,
+          typecast_exprt::conditional_cast(member_offset, pointer_diff_type())),
+        char_pointer.type());
 
       const exprt new_address_casted =
         typecast_exprt::conditional_cast(new_address, new_pointer_type);
