Merge pull request #7338 from diffblue/smt2_void_pointer_minus

SMT2 backend: minus on void pointers

Author: tautschnig

regression/cbmc/void_pointer3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend gcc-only
+CORE gcc-only
 main.c
 
 ^EXIT=0$

src/solvers/smt2/smt2_conv.cpp

@@ -3837,11 +3837,23 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
        expr.op1().type().id()==ID_pointer)
     {
       // Pointer difference
-      auto element_size =
-        pointer_offset_size(to_pointer_type(expr.op0().type()).base_type(), ns);
-      CHECK_RETURN(element_size.has_value() && *element_size >= 1);
+      const auto &base_type = to_pointer_type(expr.op0().type()).base_type();
+      mp_integer element_size;
+
+      if(base_type.id() == ID_empty)
+      {
+        // Pointer arithmetic on void 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(base_type, ns);
+        CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
+        element_size = *element_size_opt;
+      }
 
-      if(*element_size >= 2)
+      if(element_size >= 2)
         out << "(bvsdiv ";
 
       INVARIANT(
@@ -3855,8 +3867,8 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
       convert_expr(expr.op1());
       out << ")";
 
-      if(*element_size >= 2)
-        out << " (_ bv" << *element_size << " " << boolbv_width(expr.type())
+      if(element_size >= 2)
+        out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
             << "))";
     }
     else