C++ bool is at least one byte wide

regression/cpp/cprover_bool1/main.cpp

@@ -0,0 +1,12 @@
+#include <limits.h>
+
+static_assert(
+  sizeof(bool[CHAR_BIT]) >= CHAR_BIT,
+  "a bool is at least one byte wide");
+static_assert(
+  sizeof(__CPROVER_bool[CHAR_BIT]) == 1,
+  "__CPROVER_bool is just a single bit");
+
+int main(int argc, char *argv[])
+{
+}

regression/cpp/cprover_bool1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+-std=c++11
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/cpp/cpp_convert_type.cpp

@@ -104,7 +104,7 @@ void cpp_convert_typet::read_rec(const typet &type)
     int128_cnt++;
   else if(type.id()==ID_complex)
     complex_cnt++;
-  else if(type.id()==ID_bool)
+  else if(type.id() == ID_c_bool)
     cpp_bool_cnt++;
   else if(type.id()==ID_proper_bool)
     proper_bool_cnt++;
@@ -414,7 +414,7 @@ void cpp_convert_typet::write(typet &type)
        int64_cnt || int128_cnt || ptr32_cnt || ptr64_cnt)
       throw "illegal type modifier for C++ bool";
 
-    type.id(ID_bool);
+    type = c_bool_type();
   }
   else if(proper_bool_cnt)
   {
@@ -603,6 +603,10 @@ void cpp_convert_plain_type(typet &type)
     // doesn't guarantee that
     type.set(ID_width, config.ansi_c.int_width);
   }
+  else if(type.id() == ID_c_bool)
+  {
+    type.set(ID_width, config.ansi_c.bool_width);
+  }
   else
   {
     cpp_convert_typet cpp_convert_type(type);

src/cpp/cpp_type2name.cpp

@@ -13,8 +13,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <string>
 
-#include <util/type.h>
+#include <util/cprover_prefix.h>
 #include <util/std_types.h>
+#include <util/type.h>
 
 static std::string do_prefix(const std::string &s)
 {
@@ -103,8 +104,10 @@ std::string cpp_type2name(const typet &type)
 
   if(type.id()==ID_empty || type.id()==ID_void)
     result+="void";
-  else if(type.id()==ID_bool)
+  else if(type.id() == ID_c_bool)
     result+="bool";
+  else if(type.id() == ID_bool)
+    result += CPROVER_PREFIX "bool";
   else if(type.id()==ID_pointer)
   {
     if(is_reference(type))

src/cpp/cpp_typecheck_conversions.cpp

@@ -13,11 +13,12 @@ Module: C++ Language Type Checking
 
 #include <cstdlib>
 
-#include <util/config.h>
 #include <util/arith_tools.h>
-#include <util/std_types.h>
-#include <util/std_expr.h>
+#include <util/config.h>
+#include <util/expr_util.h>
 #include <util/simplify_expr.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
 
 #include <ansi-c/c_qualifiers.h>
 #include <util/c_types.h>
@@ -220,6 +221,13 @@ bool cpp_typecheckt::standard_conversion_integral_promotion(
     return true;
   }
 
+  if(expr.type().id() == ID_bool || expr.type().id() == ID_c_bool)
+  {
+    new_expr = expr;
+    new_expr.make_typecast(int_type);
+    return true;
+  }
+
   if(expr.type().id()==ID_c_enum_tag)
   {
     new_expr=expr;
@@ -301,11 +309,13 @@ bool cpp_typecheckt::standard_conversion_integral_conversion(
      type.id()!=ID_unsignedbv)
       return false;
 
-  if(expr.type().id()!=ID_signedbv &&
-     expr.type().id()!=ID_unsignedbv &&
-     expr.type().id()!=ID_bool &&
-     expr.type().id()!=ID_c_enum_tag)
+  if(
+    expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
+    expr.type().id() != ID_c_bool && expr.type().id() != ID_bool &&
+    expr.type().id() != ID_c_enum_tag)
+  {
     return false;
+  }
 
   if(expr.get_bool(ID_C_lvalue))
     return false;
@@ -632,16 +642,18 @@ bool cpp_typecheckt::standard_conversion_boolean(
   if(expr.get_bool(ID_C_lvalue))
     return false;
 
-  if(expr.type().id()!=ID_signedbv &&
-     expr.type().id()!=ID_unsignedbv &&
-     expr.type().id()!=ID_pointer &&
-     expr.type().id()!=ID_c_enum_tag)
+  if(
+    expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
+    expr.type().id() != ID_pointer && expr.type().id() != ID_bool &&
+    expr.type().id() != ID_c_enum_tag)
+  {
     return false;
+  }
 
   c_qualifierst qual_from;
   qual_from.read(expr.type());
 
-  bool_typet Bool;
+  typet Bool = c_bool_type();
   qual_from.write(Bool);
 
   new_expr=expr;
@@ -781,13 +793,19 @@ bool cpp_typecheckt::standard_conversion_sequence(
 
       rank += 3;
     }
-    else if(type.id()==ID_bool)
+    else if(type.id() == ID_c_bool)
     {
       if(!standard_conversion_boolean(curr_expr, new_expr))
         return false;
 
       rank += 3;
     }
+    else if(type.id() == ID_bool)
+    {
+      new_expr = is_not_zero(curr_expr, *this);
+
+      rank += 3;
+    }
     else
       return false;
   }
@@ -1794,11 +1812,10 @@ bool cpp_typecheckt::reinterpret_typecast(
     return true;
   }
 
-  if((e.type().id()==ID_unsignedbv ||
-      e.type().id()==ID_signedbv ||
-      e.type().id()==ID_bool) &&
-     type.id()==ID_pointer &&
-     !is_reference(type))
+  if(
+    (e.type().id() == ID_unsignedbv || e.type().id() == ID_signedbv ||
+     e.type().id() == ID_c_bool || e.type().id() == ID_bool) &&
+    type.id() == ID_pointer && !is_reference(type))
   {
     // integer to pointer
     if(simplify_expr(e, *this).is_zero())

src/cpp/cpp_typecheck_resolve.cpp

@@ -970,12 +970,10 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_scope(
       irept::subt::const_iterator next=pos+1;
       assert(next != cpp_name.get_sub().end());
 
-      if(next->id() == ID_cpp_name ||
-         next->id() == ID_pointer ||
-         next->id() == ID_int ||
-         next->id() == ID_char ||
-         next->id() == ID_bool ||
-         next->id() == ID_merged_type)
+      if(
+        next->id() == ID_cpp_name || next->id() == ID_pointer ||
+        next->id() == ID_int || next->id() == ID_char ||
+        next->id() == ID_c_bool || next->id() == ID_merged_type)
       {
         // it's a cast operator
         irept next_ir=*next;

src/cpp/cpp_typecheck_type.cpp

@@ -178,12 +178,10 @@ void cpp_typecheckt::typecheck_type(typet &type)
   {
     typecheck_c_bit_field_type(to_c_bit_field_type(type));
   }
-  else if(type.id()==ID_unsignedbv ||
-          type.id()==ID_signedbv ||
-          type.id()==ID_bool ||
-          type.id()==ID_floatbv ||
-          type.id()==ID_fixedbv ||
-          type.id()==ID_empty)
+  else if(
+    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+    type.id() == ID_bool || type.id() == ID_c_bool || type.id() == ID_floatbv ||
+    type.id() == ID_fixedbv || type.id() == ID_empty)
   {
   }
   else if(type.id() == ID_symbol_type)

src/cpp/expr2cpp.cpp

@@ -110,7 +110,7 @@ std::string expr2cppt::convert_constant(
   const constant_exprt &src,
   unsigned &precedence)
 {
-  if(src.type().id()==ID_bool)
+  if(src.type().id() == ID_c_bool)
   {
     // C++ has built-in Boolean constants, in contrast to C
     if(src.is_true())
@@ -347,6 +347,10 @@ std::string expr2cppt::convert_rec(
     // only really used in error messages
     return "{ ... }";
   }
+  else if(src.id() == ID_c_bool)
+  {
+    return q + "bool" + d;
+  }
   else
     return expr2ct::convert_rec(src, qualifiers, declarator);
 }

src/cpp/parse.cpp

@@ -2453,7 +2453,9 @@ bool Parser::optIntegralTypeOrClassSpec(typet &p)
     case TOK_GCC_INT128: type_id=ID_gcc_int128; break;
     case TOK_GCC_FLOAT80: type_id=ID_gcc_float80; break;
     case TOK_GCC_FLOAT128: type_id=ID_gcc_float128; break;
-    case TOK_BOOL: type_id=ID_bool; break;
+    case TOK_BOOL:
+      type_id = ID_c_bool;
+      break;
     case TOK_CPROVER_BOOL: type_id=ID_proper_bool; break;
     case TOK_AUTO: type_id = ID_auto; break;
     default: type_id=irep_idt();
@@ -6713,7 +6715,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
 
   case TOK_TRUE:
     lex.get_token(tk);
-    exp=true_exprt();
+    exp = typecast_exprt(true_exprt(), c_bool_type());
     set_location(exp, tk);
     #ifdef DEBUG
     std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 4\n";
@@ -6722,7 +6724,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
 
   case TOK_FALSE:
     lex.get_token(tk);
-    exp=false_exprt();
+    exp = typecast_exprt(false_exprt(), c_bool_type());
     set_location(exp, tk);
     #ifdef DEBUG
     std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 5\n";