Skip to content

Commit 6fe723b

Browse files
committed
Distinguish __CPROVER_bool from _Bool in output
A __CPROVER_bool is a single bit and should not be output the same way as a _Bool, which may be one or more bytes wide.
1 parent 0107bce commit 6fe723b

File tree

3 files changed

+19
-1
lines changed

3 files changed

+19
-1
lines changed

regression/cbmc/cprover_bool1/main.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int y;
6+
__CPROVER_bool x = y;
7+
assert(x != (__CPROVER_bool)y);
8+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--trace
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
x != \(__CPROVER_bool\)y
8+
--
9+
x != \(_Bool\)y
10+
^warning: ignoring

src/ansi-c/expr2c.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ std::string expr2ct::convert_rec(
206206

207207
if(src.id()==ID_bool)
208208
{
209-
return q+"_Bool"+d;
209+
return q + CPROVER_PREFIX + "bool" + d;
210210
}
211211
else if(src.id()==ID_c_bool)
212212
{

0 commit comments

Comments
 (0)