C front-end: reject pointer subtraction over distinct types

regression/cbmc/ptr_arithmetic_on_null/main.c

@@ -12,7 +12,11 @@ void main()
   assert(NULL - NULL == 0);
 
   int *ptr;
+#ifdef MISSING_CAST
   assert(ptr - NULL == 0);
+#else
+  assert(ptr - (int *)NULL == 0);
+#endif
   ptr = NULL;
   assert((ptr - 1) + 1 == NULL);
 

regression/cbmc/ptr_arithmetic_on_null/test.desc

@@ -5,7 +5,7 @@ main.c
 ^\[main.assertion.2\] line .* assertion \(void \*\)0 != \(void \*\)0 - \(.*\)1: SUCCESS$
 ^\[main.assertion.3\] line .* assertion \(void \*\)0 != \(void \*\)0 \+ \(.*\)offset: SUCCESS$
 ^\[main.assertion.4\] line .* assertion \(void \*\)0 - \(void \*\)0 == \(.*\)0: SUCCESS$
-^\[main.assertion.5\] line .* assertion ptr - \(void \*\)0 == \(.*\)0: FAILURE$
+^\[main.assertion.5\] line .* assertion ptr - \(signed int \*\)\(void \*\)0 == \(.*\)0: FAILURE$
 ^\[main.assertion.6\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): SUCCESS$
 ^\[main.assertion.7\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): FAILURE$
 ^EXIT=10$

regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc

@@ -0,0 +1,9 @@
+CORE gcc-only
+main.c
+-DMISSING_CAST
+pointer subtraction over different types
+CONVERSION ERROR
+^EXIT=6$
+^SIGNAL=0$
+--
+--

src/ansi-c/c_typecheck_expr.cpp

@@ -4171,8 +4171,11 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
     if(type0.id()==ID_pointer &&
        type1.id()==ID_pointer)
     {
-      // We should check the subtypes, and complain if
-      // they are really different.
+      if(type0 != type1)
+      {
+        throw invalid_source_file_exceptiont{
+          "pointer subtraction over different types", expr.source_location()};
+      }
       expr.type()=pointer_diff_type();
       typecheck_arithmetic_pointer(op0);
       typecheck_arithmetic_pointer(op1);