Skip to content

Commit 7dce973

Browse files
tautschnigtautschnig
committed
C++ bool is at least one byte wide
Do not treat "bool" as a single bit, which is what __CPROVER_bool is for.
1 parent 3965d9d commit 7dce973

9 files changed

+84
-38
lines changed

‎regression/cpp/cprover_bool1/main.cpp

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <limits.h>
2+
3+
static_assert(
4+
sizeof(bool[CHAR_BIT]) >= CHAR_BIT,
5+
"a bool is at least one byte wide");
6+
static_assert(
7+
sizeof(__CPROVER_bool[CHAR_BIT]) == 1,
8+
"__CPROVER_bool is just a single bit");
9+
10+
int main(int argc, char *argv[])
11+
{
12+
}

‎regression/cpp/cprover_bool1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.cpp
3+
-std=c++11
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

‎src/cpp/cpp_convert_type.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ void cpp_convert_typet::read_rec(const typet &type)
104104
int128_cnt++;
105105
else if(type.id()==ID_complex)
106106
complex_cnt++;
107-
else if(type.id()==ID_bool)
107+
else if(type.id() == ID_c_bool)
108108
cpp_bool_cnt++;
109109
else if(type.id()==ID_proper_bool)
110110
proper_bool_cnt++;
@@ -414,7 +414,7 @@ void cpp_convert_typet::write(typet &type)
414414
int64_cnt || int128_cnt || ptr32_cnt || ptr64_cnt)
415415
throw "illegal type modifier for C++ bool";
416416

417-
type.id(ID_bool);
417+
type = c_bool_type();
418418
}
419419
else if(proper_bool_cnt)
420420
{
@@ -603,6 +603,10 @@ void cpp_convert_plain_type(typet &type)
603603
// doesn't guarantee that
604604
type.set(ID_width, config.ansi_c.int_width);
605605
}
606+
else if(type.id() == ID_c_bool)
607+
{
608+
type.set(ID_width, config.ansi_c.bool_width);
609+
}
606610
else
607611
{
608612
cpp_convert_typet cpp_convert_type(type);

‎src/cpp/cpp_type2name.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,9 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <string>
1515

16-
#include <util/type.h>
16+
#include <util/cprover_prefix.h>
1717
#include <util/std_types.h>
18+
#include <util/type.h>
1819

1920
static std::string do_prefix(const std::string &s)
2021
{
@@ -103,8 +104,10 @@ std::string cpp_type2name(const typet &type)
103104

104105
if(type.id()==ID_empty || type.id()==ID_void)
105106
result+="void";
106-
else if(type.id()==ID_bool)
107+
else if(type.id() == ID_c_bool)
107108
result+="bool";
109+
else if(type.id() == ID_bool)
110+
result += CPROVER_PREFIX "bool";
108111
else if(type.id()==ID_pointer)
109112
{
110113
if(is_reference(type))

‎src/cpp/cpp_typecheck_conversions.cpp

Lines changed: 35 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,12 @@ Module: C++ Language Type Checking
1313

1414
#include <cstdlib>
1515

16-
#include <util/config.h>
1716
#include <util/arith_tools.h>
18-
#include <util/std_types.h>
19-
#include <util/std_expr.h>
17+
#include <util/config.h>
18+
#include <util/expr_util.h>
2019
#include <util/simplify_expr.h>
20+
#include <util/std_expr.h>
21+
#include <util/std_types.h>
2122

2223
#include <ansi-c/c_qualifiers.h>
2324
#include <util/c_types.h>
@@ -220,6 +221,13 @@ bool cpp_typecheckt::standard_conversion_integral_promotion(
220221
return true;
221222
}
222223

224+
if(expr.type().id() == ID_bool || expr.type().id() == ID_c_bool)
225+
{
226+
new_expr = expr;
227+
new_expr.make_typecast(int_type);
228+
return true;
229+
}
230+
223231
if(expr.type().id()==ID_c_enum_tag)
224232
{
225233
new_expr=expr;
@@ -301,11 +309,13 @@ bool cpp_typecheckt::standard_conversion_integral_conversion(
301309
type.id()!=ID_unsignedbv)
302310
return false;
303311

304-
if(expr.type().id()!=ID_signedbv &&
305-
expr.type().id()!=ID_unsignedbv &&
306-
expr.type().id()!=ID_bool &&
307-
expr.type().id()!=ID_c_enum_tag)
312+
if(
313+
expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
314+
expr.type().id() != ID_c_bool && expr.type().id() != ID_bool &&
315+
expr.type().id() != ID_c_enum_tag)
316+
{
308317
return false;
318+
}
309319

310320
if(expr.get_bool(ID_C_lvalue))
311321
return false;
@@ -632,16 +642,18 @@ bool cpp_typecheckt::standard_conversion_boolean(
632642
if(expr.get_bool(ID_C_lvalue))
633643
return false;
634644

635-
if(expr.type().id()!=ID_signedbv &&
636-
expr.type().id()!=ID_unsignedbv &&
637-
expr.type().id()!=ID_pointer &&
638-
expr.type().id()!=ID_c_enum_tag)
645+
if(
646+
expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
647+
expr.type().id() != ID_pointer && expr.type().id() != ID_bool &&
648+
expr.type().id() != ID_c_enum_tag)
649+
{
639650
return false;
651+
}
640652

641653
c_qualifierst qual_from;
642654
qual_from.read(expr.type());
643655

644-
bool_typet Bool;
656+
typet Bool = c_bool_type();
645657
qual_from.write(Bool);
646658

647659
new_expr=expr;
@@ -781,13 +793,19 @@ bool cpp_typecheckt::standard_conversion_sequence(
781793

782794
rank += 3;
783795
}
784-
else if(type.id()==ID_bool)
796+
else if(type.id() == ID_c_bool)
785797
{
786798
if(!standard_conversion_boolean(curr_expr, new_expr))
787799
return false;
788800

789801
rank += 3;
790802
}
803+
else if(type.id() == ID_bool)
804+
{
805+
new_expr = is_not_zero(curr_expr, *this);
806+
807+
rank += 3;
808+
}
791809
else
792810
return false;
793811
}
@@ -1794,11 +1812,10 @@ bool cpp_typecheckt::reinterpret_typecast(
17941812
return true;
17951813
}
17961814

1797-
if((e.type().id()==ID_unsignedbv ||
1798-
e.type().id()==ID_signedbv ||
1799-
e.type().id()==ID_bool) &&
1800-
type.id()==ID_pointer &&
1801-
!is_reference(type))
1815+
if(
1816+
(e.type().id() == ID_unsignedbv || e.type().id() == ID_signedbv ||
1817+
e.type().id() == ID_c_bool || e.type().id() == ID_bool) &&
1818+
type.id() == ID_pointer && !is_reference(type))
18021819
{
18031820
// integer to pointer
18041821
if(simplify_expr(e, *this).is_zero())

‎src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -970,12 +970,10 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_scope(
970970
irept::subt::const_iterator next=pos+1;
971971
assert(next != cpp_name.get_sub().end());
972972

973-
if(next->id() == ID_cpp_name ||
974-
next->id() == ID_pointer ||
975-
next->id() == ID_int ||
976-
next->id() == ID_char ||
977-
next->id() == ID_bool ||
978-
next->id() == ID_merged_type)
973+
if(
974+
next->id() == ID_cpp_name || next->id() == ID_pointer ||
975+
next->id() == ID_int || next->id() == ID_char ||
976+
next->id() == ID_c_bool || next->id() == ID_merged_type)
979977
{
980978
// it's a cast operator
981979
irept next_ir=*next;

‎src/cpp/cpp_typecheck_type.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -178,12 +178,10 @@ void cpp_typecheckt::typecheck_type(typet &type)
178178
{
179179
typecheck_c_bit_field_type(to_c_bit_field_type(type));
180180
}
181-
else if(type.id()==ID_unsignedbv ||
182-
type.id()==ID_signedbv ||
183-
type.id()==ID_bool ||
184-
type.id()==ID_floatbv ||
185-
type.id()==ID_fixedbv ||
186-
type.id()==ID_empty)
181+
else if(
182+
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
183+
type.id() == ID_bool || type.id() == ID_c_bool || type.id() == ID_floatbv ||
184+
type.id() == ID_fixedbv || type.id() == ID_empty)
187185
{
188186
}
189187
else if(type.id() == ID_symbol_type)

‎src/cpp/expr2cpp.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ std::string expr2cppt::convert_constant(
110110
const constant_exprt &src,
111111
unsigned &precedence)
112112
{
113-
if(src.type().id()==ID_bool)
113+
if(src.type().id() == ID_c_bool)
114114
{
115115
// C++ has built-in Boolean constants, in contrast to C
116116
if(src.is_true())
@@ -347,6 +347,10 @@ std::string expr2cppt::convert_rec(
347347
// only really used in error messages
348348
return "{ ... }";
349349
}
350+
else if(src.id() == ID_c_bool)
351+
{
352+
return q + "bool" + d;
353+
}
350354
else
351355
return expr2ct::convert_rec(src, qualifiers, declarator);
352356
}

‎src/cpp/parse.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2453,7 +2453,9 @@ bool Parser::optIntegralTypeOrClassSpec(typet &p)
24532453
case TOK_GCC_INT128: type_id=ID_gcc_int128; break;
24542454
case TOK_GCC_FLOAT80: type_id=ID_gcc_float80; break;
24552455
case TOK_GCC_FLOAT128: type_id=ID_gcc_float128; break;
2456-
case TOK_BOOL: type_id=ID_bool; break;
2456+
case TOK_BOOL:
2457+
type_id = ID_c_bool;
2458+
break;
24572459
case TOK_CPROVER_BOOL: type_id=ID_proper_bool; break;
24582460
case TOK_AUTO: type_id = ID_auto; break;
24592461
default: type_id=irep_idt();
@@ -6713,7 +6715,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
67136715

67146716
case TOK_TRUE:
67156717
lex.get_token(tk);
6716-
exp=true_exprt();
6718+
exp = typecast_exprt(true_exprt(), c_bool_type());
67176719
set_location(exp, tk);
67186720
#ifdef DEBUG
67196721
std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 4\n";
@@ -6722,7 +6724,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
67226724

67236725
case TOK_FALSE:
67246726
lex.get_token(tk);
6725-
exp=false_exprt();
6727+
exp = typecast_exprt(false_exprt(), c_bool_type());
67266728
set_location(exp, tk);
67276729
#ifdef DEBUG
67286730
std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 5\n";

0 commit comments

Comments
 (0)