Merge pull request #2729 from tautschnig/add-sub-conflict

Use pointer difference type when adding to pointer

Author: tautschnig

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;
+}

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

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);