document why sizeof(void) works

NathanJPhillips · Jun 5, 2018 · 6eab2f9 · 6eab2f9
1 parent e8d26ae
commit 6eab2f9
Show file tree

Hide file tree

Showing 2 changed files with 52 additions and 22 deletions.
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -935,26 +935,30 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
     throw 0;
   }
 
+  exprt new_expr;
+
   if(type.id()==ID_c_bit_field)
   {
     err_location(expr);
     error() << "sizeof cannot be applied to bit fields" << eom;
     throw 0;
   }
-
-  if(type.id()==ID_empty &&
-     expr.operands().size()==1 &&
-     expr.op0().id()==ID_dereference &&
-     expr.op0().op0().type()==pointer_type(void_type()))
-    type=char_type();
-
-  exprt new_expr=size_of_expr(type, *this);
-
-  if(new_expr.is_nil())
+  else if(type.id() == ID_empty)
   {
-    err_location(expr);
-    error() << "type has no size: " << to_string(type) << eom;
-    throw 0;
+    // This is a gcc extension.
+    // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+    new_expr = size_of_expr(char_type(), *this);
+  }
+  else
+  {
+    new_expr = size_of_expr(type, *this);
+
+    if(new_expr.is_nil())
+    {
+      err_location(expr);
+      error() << "type has no size: " << to_string(type) << eom;
+      throw 0;
+    }
   }
 
   new_expr.swap(expr);

diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
@@ -348,10 +348,18 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
         CHECK_RETURN(bv.size()==bits);
 
         typet pointer_sub_type=it->type().subtype();
+
         if(pointer_sub_type.id()==ID_empty)
-          pointer_sub_type=char_type();
-        size=pointer_offset_size(pointer_sub_type, ns);
-        CHECK_RETURN(size>0);
+        {
+          // This is a gcc extension.
+          // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+          size = 1;
+        }
+        else
+        {
+          size = pointer_offset_size(pointer_sub_type, ns);
+          CHECK_RETURN(size > 0);
+        }
       }
     }
 
@@ -423,10 +431,19 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     bv=convert_bv(expr.op0());
 
     typet pointer_sub_type=expr.op0().type().subtype();
+    mp_integer element_size;
+
     if(pointer_sub_type.id()==ID_empty)
-      pointer_sub_type=char_type();
-    mp_integer element_size=pointer_offset_size(pointer_sub_type, ns);
-    DATA_INVARIANT(element_size>0, "object size expected to be positive");
+    {
+      // This is a gcc extension.
+      // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+      element_size = 1;
+    }
+    else
+    {
+      element_size = pointer_offset_size(pointer_sub_type, ns);
+      DATA_INVARIANT(element_size > 0, "object size expected to be positive");
+    }
 
     offset_arithmetic(bv, element_size, neg_op1);
 
@@ -488,10 +505,19 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     bvt bv=bv_utils.sub(op0, op1);
 
     typet pointer_sub_type=expr.op0().type().subtype();
+    mp_integer element_size;
+
     if(pointer_sub_type.id()==ID_empty)
-      pointer_sub_type=char_type();
-    mp_integer element_size=pointer_offset_size(pointer_sub_type, ns);
-    DATA_INVARIANT(element_size>0, "object size expected to be positive");
+    {
+      // This is a gcc extension.
+      // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+      element_size = 1;
+    }
+    else
+    {
+      element_size = pointer_offset_size(pointer_sub_type, ns);
+      DATA_INVARIANT(element_size > 0, "object size expected to be positive");
+    }
 
     if(element_size!=1)
     {