Evaluating sizeof over __CPROVER_bool requires special cases

__CPROVER_bool is just a single bit, and not part of any language standard
describing the semantics of sizeof. We can declare arrays of __CPROVER_bool,
which will thus have elements that are not aligned on byte boundaries. Using
sizeof with such an array thus requires specific handling.

Author: tautschnig

src/ansi-c/c_typecheck_expr.cpp

@@ -979,7 +979,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
 
   exprt new_expr;
 
-  if(type.id()==ID_c_bit_field)
+  if(type.id() == ID_c_bit_field || type.id() == ID_bool)
   {
     err_location(expr);
     error() << "sizeof cannot be applied to bit fields" << eom;
@@ -1739,7 +1739,7 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)
 
   exprt &op=expr.op0();
 
-  if(op.type().id()==ID_c_bit_field)
+  if(op.type().id() == ID_c_bit_field || op.type().id() == ID_bool)
   {
     err_location(expr);
     error() << "cannot take address of a bit field" << eom;

src/util/pointer_offset_size.cpp

@@ -305,6 +305,13 @@ exprt member_offset_expr(
       if(bytes > 0)
         result = plus_exprt(result, from_integer(bytes, result.type()));
     }
+    else if(c.type().id() == ID_bool)
+    {
+      ++bit_field_bits;
+      const std::size_t bytes = bit_field_bits / 8;
+      bit_field_bits %= 8;
+      result = plus_exprt(result, from_integer(bytes, result.type()));
+    }
     else
     {
       DATA_INVARIANT(
@@ -427,6 +434,13 @@ exprt size_of_expr(
         if(bytes > 0)
           result = plus_exprt(result, from_integer(bytes, result.type()));
       }
+      else if(c.type().id() == ID_bool)
+      {
+        ++bit_field_bits;
+        const std::size_t bytes = bit_field_bits / 8;
+        bit_field_bits %= 8;
+        result = plus_exprt(result, from_integer(bytes, result.type()));
+      }
       else
       {
         DATA_INVARIANT(