diff --git a/src/kernel_internals/runtime/machdeps.ml b/src/kernel_internals/runtime/machdeps.ml
index 3c9da30d57534a6e73ebe343faebe911a21929a6..e0600a7d1a86c11d91df32dc7b6a85bba75c8e02 100644
--- a/src/kernel_internals/runtime/machdeps.ml
+++ b/src/kernel_internals/runtime/machdeps.ml
@@ -56,7 +56,7 @@ let x86_16 = {
   sizeof_float     = 4;
   sizeof_double    = 8;
   sizeof_longdouble  = 16;
-  sizeof_void      = 1;
+  sizeof_void      = -1;
   sizeof_fun       = -1;
   size_t = "unsigned int";
   wchar_t = "int";
@@ -83,7 +83,7 @@ let x86_16 = {
 
 let gcc_x86_16 = { x86_16 with
                    compiler = "gcc";
-                   sizeof_fun = 1; alignof_fun = 1;
+                   sizeof_void = 1; sizeof_fun = 1; alignof_fun = 1;
                  }
 
 let x86_32 = {
@@ -98,7 +98,7 @@ let x86_32 = {
   sizeof_float     = 4;
   sizeof_double    = 8;
   sizeof_longdouble  = 12;
-  sizeof_void      = 1;
+  sizeof_void      = -1;
   sizeof_fun       = -1;
   size_t = "unsigned int";
   wchar_t = "int";
@@ -123,7 +123,7 @@ let x86_32 = {
 
 let gcc_x86_32 = { x86_32 with
                    compiler = "gcc";
-                   sizeof_fun = 1; alignof_fun = 1;
+                   sizeof_void = 1; sizeof_fun = 1; alignof_fun = 1;
                  }
 
 let x86_64 = {
@@ -138,7 +138,7 @@ let x86_64 = {
   sizeof_float     = 4;
   sizeof_double    = 8;
   sizeof_longdouble  = 16;
-  sizeof_void      = 1;
+  sizeof_void      = -1;
   sizeof_fun       = -1;
   size_t = "unsigned long";
   wchar_t = "int";
@@ -163,7 +163,7 @@ let x86_64 = {
 
 let gcc_x86_64 = { x86_64 with
                    compiler = "gcc";
-                   sizeof_fun = 1; alignof_fun = 1;
+                   sizeof_void = 1; sizeof_fun = 1; alignof_fun = 1;
                  }
 
 let ppc_32 = {
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index 5af81b797eb191fe248f54761c7d5580eeead488..05491e1df7a2c74275341269f94c4385630e1bbd 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -219,8 +219,11 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
     | TVoid _ | TBuiltin_va_list _ | TNamed _ | TFun (_, _, _, _) as typ ->
         let size =
           match bfinfo with
-            | Other -> Integer.of_int (bitsSizeOf typ)
-            | Bitfield i -> Integer.of_int64 i
+          | Other -> begin
+            try Integer.of_int (bitsSizeOf typ)
+            with Cil.SizeOfError _ -> Integer.zero
+          end
+          | Bitfield i -> Integer.of_int64 i
         in
         (if Integer.is_zero start
            && Integer.equal size req_size then
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 203845899acaf1d53dd33ff0b842fd4c93081eb5..6370d0abcc1a6f753b1bdca5093f15f2b7b3d822 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4409,7 +4409,11 @@ and bitsSizeOf t =
              sz' (*WAS: addTrailing sz' (8 * bytesAlignOf t)*)
            | _ -> raise (SizeOfError ("Array with non-constant length.", t))
          end)
-  | TVoid _ -> 8 * theMachine.theMachine.sizeof_void
+  | TVoid _ ->
+    if theMachine.theMachine.sizeof_void >= 0 then
+      8 * theMachine.theMachine.sizeof_void
+    else
+      raise (SizeOfError ("Undefined sizeof(void).", t))
   | TFun _ ->
     if theMachine.theMachine.sizeof_fun >= 0 then
       8 * theMachine.theMachine.sizeof_fun
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 5d1fcf6df5ba8b1b970c07a1839698788108074b..8d5ce416adc74c1837981b6b097af5aed429dc8f 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -272,7 +272,7 @@ let print_machdep fmt (m : Cil_types.mach) =
         "double", m.sizeof_double, m.alignof_double ;
         "long double", m.sizeof_longdouble, m.alignof_longdouble ;
         "pointer", m.sizeof_ptr, m.alignof_ptr ;
-        "void", m.sizeof_void, 1 ;
+        "void", m.sizeof_void, m.sizeof_void ;
         "function", m.sizeof_fun, m.alignof_fun ;
       ] ;
     List.iter
diff --git a/tests/constant_propagation/oracle/array_pointers.res.oracle b/tests/constant_propagation/oracle/array_pointers.res.oracle
index 13db6ccd08dd6658eb48720410f5beed80842700..fb141388d4db6867146e35d35b88e5b0da06c19d 100644
--- a/tests/constant_propagation/oracle/array_pointers.res.oracle
+++ b/tests/constant_propagation/oracle/array_pointers.res.oracle
@@ -12,7 +12,7 @@
 [eva:final-states] Values at end of function main:
   q ∈ {{ &p + {4} }}
   r ∈ {{ &p + {8} }}
-  s ∈ {1}
+  s ∈ [--..--]
 [scf] beginning constant propagation
 [kernel] tests/constant_propagation/array_pointers.i:10: Warning: 
   using size of 'void'
diff --git a/tests/misc/oracle/print_machdep.res.oracle b/tests/misc/oracle/print_machdep.res.oracle
index e0ef03b220dadd48a509cd8d00a25151499d3f9b..7c9a04850ea7f793b0235931ec0b95c651c2cead 100644
--- a/tests/misc/oracle/print_machdep.res.oracle
+++ b/tests/misc/oracle/print_machdep.res.oracle
@@ -7,7 +7,7 @@ Machine: gcc 4.0.3 AMD64
    sizeof      double =  8 (64 bits, aligned on 64 bits)
    sizeof long double = 16 (128 bits, aligned on 128 bits)
    sizeof     pointer =  8 (64 bits, aligned on 64 bits)
-   sizeof        void =  1 (8 bits, aligned on 8 bits)
+   sizeof        void = error (alignof error)
    sizeof    function = error (alignof error)
    typeof   sizeof(T) = unsigned long
    typeof     wchar_t = int