[smt2_convt] Fix invalid and NULL pointer handling

regression/cbmc/memset_null/main.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+#include <string.h>
+
+void main()
+{
+  char *data = nondet() ? NULL : malloc(8);
+  memset(data, 0, 8);
+  memset(data, 0, 8);
+}

regression/cbmc/memset_null/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\[main.precondition_instance.1\] line .* memset destination region writeable: FAILURE$
+^\[main.precondition_instance.2\] line .* memset destination region writeable: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test case checks that byte operations (e.g. memset) oninvalid and `NULL`
+pointers are correctly encoded in SMT2.

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
@@ -4236,6 +4247,11 @@ void smt2_convt::set_to(const exprt &expr, bool value)
   if(expr.id() == ID_equal && value)
   {
     const equal_exprt &equal_expr=to_equal_expr(expr);
+    if(equal_expr.lhs().type().id() == ID_empty)
+    {
+      // ignore equality checking over expressions with empty (void) type
+      return;
+    }
 
     if(equal_expr.lhs().id()==ID_symbol)
     {