[smt2_convt] Fix arithmetic on invalid pointers

CBMC crashed on SMT2 conversion of pointer arithmetic on NULL and other kinds
of invalid pointers.
This change fixes the encoding of pointer arithmetic on invalid pointers.

Author: SaswatPadhi

regression/cbmc/ptr_arithmetic_on_null/main.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+
+void main()
+{
+  assert(NULL != (NULL + 1));
+  assert(NULL != (NULL - 1));
+
+  int offset;
+  __CPROVER_assume(offset != 0);
+  assert(NULL != (NULL + offset));
+
+  assert(NULL - NULL == 0);
+
+  int *ptr;
+  assert(ptr - NULL == 0);
+  ptr = NULL;
+  assert((ptr - 1) + 1 == NULL);
+
+  ptr = nondet() ? NULL : malloc(1);
+  assert((ptr - 1) + 1 == (NULL + 1) - 1);
+}

regression/cbmc/ptr_arithmetic_on_null/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+
+^\[main.assertion.1\] line .* assertion \(void \*\)0 != \(void \*\)0 \+ \(.*\)1: SUCCESS$
+^\[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.6\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): SUCCESS$
+^\[main.assertion.7\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test case checks that pointer arithmetic on NULL pointers are correctly
+encoded by the SMT2 translation routines.

src/solvers/smt2/smt2_conv.cpp

@@ -3162,18 +3162,29 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
         p.type().id() == ID_pointer,
         "one of the operands should have pointer type");
 
-      const auto element_size = pointer_offset_size(expr.type().subtype(), ns);
-      CHECK_RETURN(element_size.has_value() && *element_size >= 1);
+      mp_integer element_size;
+      if(expr.type().subtype().id() == ID_empty)
+      {
+        // This is a gcc extension.
+        // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+        element_size = 1;
+      }
+      else
+      {
+        auto element_size_opt = pointer_offset_size(expr.type().subtype(), ns);
+        CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
+        element_size = *element_size_opt;
+      }
 
       out << "(bvadd ";
       convert_expr(p);
       out << " ";
 
-      if(*element_size >= 2)
+      if(element_size >= 2)
       {
         out << "(bvmul ";
         convert_expr(i);
-        out << " (_ bv" << *element_size << " " << boolbv_width(expr.type())
+        out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
             << "))";
       }
       else