Skip to content

Commit 6ee8f9d

Browse files
kroeningkroening
committed
C23 keywords
This adds scanner, parser and typechecker support for the new C23 keywords.
1 parent 0b000a3 commit 6ee8f9d

34 files changed

+422
-95
lines changed

‎README.md

+8-7
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,14 @@
66
About
77
=====
88

9-
CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99,
10-
most of C11 and most compiler extensions provided by gcc and Visual Studio. It
11-
also supports SystemC using Scoot. It allows verifying array bounds (buffer
12-
overflows), pointer safety, exceptions and user-specified assertions.
13-
Furthermore, it can check C and C++ for consistency with other languages, such
14-
as Verilog. The verification is performed by unwinding the loops in the program
15-
and passing the resulting equation to a decision procedure.
9+
CBMC is a Bounded Model Checker for C and C++ programs. It supports C89,
10+
C99, most of C11, C17, C23 and most compiler extensions provided by gcc and
11+
Visual Studio. It also supports SystemC using Scoot. It allows verifying
12+
array bounds (buffer overflows), pointer safety, exceptions and
13+
user-specified assertions. Furthermore, it can check C and C++ for
14+
consistency with other languages, such as Verilog. The verification is
15+
performed by unwinding the loops in the program and passing the resulting
16+
equation to a decision procedure.
1617

1718
For full information see [cprover.org](http://www.cprover.org/cbmc).
1819

‎doc/architectural/front-page.md

+8-7
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,14 @@ website</a>; contributors should use the
88
<a href="https://github.com/diffblue/cbmc">repository</a> hosted on GitHub. CBMC
99
is part of CProver.
1010

11-
CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99,
12-
most of C11 and most compiler extensions provided by gcc and Visual Studio. It
13-
also supports SystemC using Scoot. It allows verifying array bounds (buffer
14-
overflows), pointer safety, arithmetic exceptions and user-specified assertions.
15-
Furthermore, it can check C and C++ for consistency with other languages, such
16-
as Verilog. The verification is performed by unwinding the loops in the program
17-
and passing the resulting equation to a decision procedure.
11+
CBMC is a Bounded Model Checker for C and C++ programs. It supports C89,
12+
C99, most of C11, C17, C23 and most compiler extensions provided by gcc and
13+
Visual Studio. It also supports SystemC using Scoot. It allows verifying
14+
array bounds (buffer overflows), pointer safety, arithmetic exceptions and
15+
user-specified assertions. Furthermore, it can check C and C++ for
16+
consistency with other languages, such as Verilog. The verification is
17+
performed by unwinding the loops in the program and passing the resulting
18+
equation to a decision procedure.
1819

1920
For further information see [cprover.org](http://www.cprover.org/cbmc).
2021

‎doc/man/cbmc.1

+1-1
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,7 @@ set include file (C/C++)
154154
\fB\-D\fR macro
155155
define preprocessor macro (C/C++)
156156
.TP
157-
\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR
157+
\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR, \fB\-\-c17\fR, \fB\-\-c23\fR
158158
set C language standard (default: c11)
159159
.TP
160160
\fB\-\-cpp98\fR, \fB\-\-cpp03\fR, \fB\-\-cpp11\fR

‎doc/man/goto-analyzer.1

+1-1
Original file line numberDiff line numberDiff line change
@@ -425,7 +425,7 @@ set include file (C/C++)
425425
\fB\-D\fR macro
426426
define preprocessor macro (C/C++)
427427
.TP
428-
\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR
428+
\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR, \fB\-\-c17\fR, \fB\-\-c23\fR
429429
set C language standard (default: c11)
430430
.TP
431431
\fB\-\-cpp98\fR, \fB\-\-cpp03\fR, \fB\-\-cpp11\fR

‎regression/cbmc/_BitInt/_BitInt1.c

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
// _BitInt is a C23 feature
2+
3+
// sizeof
4+
static_assert(sizeof(unsigned _BitInt(1)) == 1);
5+
static_assert(sizeof(_BitInt(32)) == 4);
6+
static_assert(sizeof(_BitInt(33)) == 8);
7+
static_assert(sizeof(_BitInt(65)) == 16);
8+
static_assert(sizeof(_BitInt(128)) == 16);
9+
10+
int main()
11+
{
12+
return 0;
13+
}

‎regression/cbmc/_BitInt/_BitInt1.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
_BitInt1.c
3+
--c23
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

‎regression/cbmc/_BitInt/_BitInt2.c

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// _BitInt is a C23 feature
2+
#include <assert.h>
3+
4+
int main()
5+
{
6+
// casts
7+
// assert((_BitInt(4))17 == 1);
8+
// assert((_BitInt(4)) - 1 == -1);
9+
// assert((unsigned _BitInt(4)) - 1 == 15);
10+
11+
// promotion (or lack thereof)
12+
// assert((unsigned _BitInt(4))15 + (unsigned _BitInt(4))1 == 0);
13+
// assert((unsigned _BitInt(4))15 + (unsigned _BitInt(5))1 == 16);
14+
// assert((unsigned _BitInt(4))15 + (signed _BitInt(5))1 == -16);
15+
// assert((unsigned _BitInt(4))15 + 1 == 16);
16+
17+
return 0;
18+
}

‎regression/cbmc/_BitInt/_BitInt2.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
_BitInt2.c
3+
--c23
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$
9+
--
10+
_BitInt implementation is missing.

‎regression/cbmc/_BitInt/_BitInt3.c

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// _BitInt is a C23 feature
2+
#include <assert.h>
3+
4+
int main()
5+
{
6+
// pointers
7+
_BitInt(3) x, *p = &x;
8+
*p = 1;
9+
10+
return 0;
11+
}

‎regression/cbmc/_BitInt/_BitInt3.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
_BitInt3.c
3+
--c23
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$
9+
--
10+
_BitInt implementation is missing.

‎regression/cbmc/_BitInt/_BitInt4.c

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// _BitInt is a C23 feature
2+
3+
static_assert(6uwb + -6wb == 0);
4+
static_assert(sizeof(255uwb + 1uwb) == 1);
5+
static_assert(sizeof(0b1111'1111uwb) == 1);
6+
7+
int main()
8+
{
9+
return 0;
10+
}

‎regression/cbmc/_BitInt/_BitInt4.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
_BitInt4.c
3+
--c23
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$
9+
--
10+
_BitInt implementation is missing.

‎regression/cbmc/constants/predefined-constants1.c

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// C23 predefined constants
2+
static_assert(!false, "false");
3+
static_assert(true, "true");
4+
static_assert(sizeof(false) == sizeof(bool), "sizeof false");
5+
static_assert(sizeof(true) == sizeof(bool), "sizeof true");
6+
static_assert(nullptr == 0, "nullptr");
7+
8+
int main()
9+
{
10+
}

‎regression/cbmc/constants/predefined-constants1.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
predefined-constants1.c
3+
--c23
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring

‎regression/cbmc/static_assert/static_assert1.c

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// C23 introduces the "static_assert" keyword.
2+
3+
struct S
4+
{
5+
// Visual Studio does not support static_assert in compound bodies.
6+
#ifndef _MSC_VER
7+
static_assert(1, "in struct");
8+
#endif
9+
int x;
10+
} asd;
11+
12+
static_assert(1, "global scope");
13+
14+
int main()
15+
{
16+
static_assert(1, "in function");
17+
}

‎regression/cbmc/static_assert/static_assert1.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
static_assert1.c
3+
--c23
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

‎regression/cbmc/typeof/typeof2.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
typedef int INTTYPE;
2+
3+
int func1();
4+
5+
// C23 typeof
6+
typeof(int) v1;
7+
typeof(INTTYPE) v2;
8+
typeof(v2) v3;
9+
typeof(1 + 1) v4;
10+
typeof(1 + 1 + func1()) v5;
11+
const typeof(int) v6;
12+
typeof(int) const v7;
13+
static typeof(int) const v8;
14+
static typeof(int) const *v9;
15+
static volatile typeof(int) const *v10;
16+
17+
void func2(typeof(int) *some_arg)
18+
{
19+
}
20+
21+
int main()
22+
{
23+
}

‎regression/cbmc/typeof/typeof2.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
typeof2.c
3+
--c23
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

‎src/ansi-c/ansi_c_convert_type.cpp

+42-29
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)
7777
int32_cnt++;
7878
else if(type.id()==ID_int64)
7979
int64_cnt++;
80+
else if(type.id() == ID_c_bitint)
81+
{
82+
bitint_cnt++;
83+
const exprt &size_expr = static_cast<const exprt &>(type.find(ID_size));
84+
85+
bv_width = size_expr;
86+
}
8087
else if(type.id()==ID_gcc_float16)
8188
gcc_float16_cnt++;
8289
else if(type.id()==ID_gcc_float32)
@@ -290,15 +297,13 @@ void ansi_c_convert_typet::write(typet &type)
290297

291298
if(!other.empty())
292299
{
293-
if(double_cnt || float_cnt || signed_cnt ||
294-
unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
295-
short_cnt || char_cnt || complex_cnt || long_cnt ||
296-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
297-
gcc_float16_cnt ||
298-
gcc_float32_cnt || gcc_float32x_cnt ||
299-
gcc_float64_cnt || gcc_float64x_cnt ||
300-
gcc_float128_cnt || gcc_float128x_cnt ||
301-
gcc_int128_cnt || bv_cnt)
300+
if(
301+
double_cnt || float_cnt || signed_cnt || unsigned_cnt || int_cnt ||
302+
c_bool_cnt || proper_bool_cnt || bitint_cnt || short_cnt || char_cnt ||
303+
complex_cnt || long_cnt || int8_cnt || int16_cnt || int32_cnt ||
304+
int64_cnt || gcc_float16_cnt || gcc_float32_cnt || gcc_float32x_cnt ||
305+
gcc_float64_cnt || gcc_float64x_cnt || gcc_float128_cnt ||
306+
gcc_float128x_cnt || gcc_int128_cnt || bv_cnt)
302307
{
303308
log.error().source_location = source_location;
304309
log.error() << "illegal type modifier for defined type" << messaget::eom;
@@ -373,10 +378,10 @@ void ansi_c_convert_typet::write(typet &type)
373378
gcc_float64_cnt || gcc_float64x_cnt ||
374379
gcc_float128_cnt || gcc_float128x_cnt)
375380
{
376-
if(signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
377-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
378-
gcc_int128_cnt || bv_cnt ||
379-
short_cnt || char_cnt)
381+
if(
382+
signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
383+
bitint_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
384+
gcc_int128_cnt || bv_cnt || short_cnt || char_cnt)
380385
{
381386
log.error().source_location = source_location;
382387
log.error() << "cannot combine integer type with floating-point type"
@@ -415,10 +420,10 @@ void ansi_c_convert_typet::write(typet &type)
415420
}
416421
else if(double_cnt || float_cnt)
417422
{
418-
if(signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
419-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
420-
gcc_int128_cnt|| bv_cnt ||
421-
short_cnt || char_cnt)
423+
if(
424+
signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
425+
bitint_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
426+
gcc_int128_cnt || bv_cnt || short_cnt || char_cnt)
422427
{
423428
log.error().source_location = source_location;
424429
log.error() << "cannot combine integer type with floating-point type"
@@ -460,10 +465,10 @@ void ansi_c_convert_typet::write(typet &type)
460465
}
461466
else if(c_bool_cnt)
462467
{
463-
if(signed_cnt || unsigned_cnt || int_cnt || short_cnt ||
464-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
465-
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
466-
char_cnt || long_cnt)
468+
if(
469+
signed_cnt || unsigned_cnt || int_cnt || short_cnt || bitint_cnt ||
470+
int8_cnt || int16_cnt || int32_cnt || int64_cnt || gcc_float128_cnt ||
471+
bv_cnt || proper_bool_cnt || char_cnt || long_cnt)
467472
{
468473
log.error().source_location = source_location;
469474
log.error() << "illegal type modifier for C boolean type"
@@ -475,10 +480,10 @@ void ansi_c_convert_typet::write(typet &type)
475480
}
476481
else if(proper_bool_cnt)
477482
{
478-
if(signed_cnt || unsigned_cnt || int_cnt || short_cnt ||
479-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
480-
gcc_float128_cnt || bv_cnt ||
481-
char_cnt || long_cnt)
483+
if(
484+
signed_cnt || unsigned_cnt || int_cnt || short_cnt || bitint_cnt ||
485+
int8_cnt || int16_cnt || int32_cnt || int64_cnt || gcc_float128_cnt ||
486+
bv_cnt || char_cnt || long_cnt)
482487
{
483488
log.error().source_location = source_location;
484489
log.error() << "illegal type modifier for proper boolean type"
@@ -496,9 +501,9 @@ void ansi_c_convert_typet::write(typet &type)
496501
}
497502
else if(char_cnt)
498503
{
499-
if(int_cnt || short_cnt || long_cnt ||
500-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
501-
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
504+
if(
505+
int_cnt || short_cnt || long_cnt || bitint_cnt || int8_cnt || int16_cnt ||
506+
int32_cnt || int64_cnt || gcc_float128_cnt || bv_cnt || proper_bool_cnt)
502507
{
503508
log.error().source_location = source_location;
504509
log.error() << "illegal type modifier for char type" << messaget::eom;
@@ -537,7 +542,9 @@ void ansi_c_convert_typet::write(typet &type)
537542

538543
if(int8_cnt || int16_cnt || int32_cnt || int64_cnt)
539544
{
540-
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
545+
if(
546+
long_cnt || char_cnt || short_cnt || bitint_cnt || gcc_int128_cnt ||
547+
bv_cnt)
541548
{
542549
log.error().source_location = source_location;
543550
log.error() << "conflicting type modifiers" << messaget::eom;
@@ -574,6 +581,12 @@ void ansi_c_convert_typet::write(typet &type)
574581
else
575582
type=gcc_unsigned_int128_type();
576583
}
584+
else if(bitint_cnt)
585+
{
586+
// explicitly-given expression for the number of value bits
587+
type.id(is_signed ? ID_c_signed_bitint : ID_c_unsigned_bitint);
588+
type.set(ID_width, bv_width);
589+
}
577590
else if(bv_cnt)
578591
{
579592
// explicitly-given expression for width

‎src/ansi-c/ansi_c_convert_type.h

+3-4
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,8 @@ class message_handlert;
2424
class ansi_c_convert_typet
2525
{
2626
public:
27-
unsigned unsigned_cnt, signed_cnt, char_cnt,
28-
int_cnt, short_cnt, long_cnt,
29-
double_cnt, float_cnt, c_bool_cnt,
30-
proper_bool_cnt, complex_cnt;
27+
unsigned unsigned_cnt, signed_cnt, char_cnt, int_cnt, short_cnt, long_cnt,
28+
double_cnt, float_cnt, c_bool_cnt, proper_bool_cnt, complex_cnt, bitint_cnt;
3129

3230
// extensions
3331
unsigned int8_cnt, int16_cnt, int32_cnt, int64_cnt,
@@ -87,6 +85,7 @@ class ansi_c_convert_typet
8785
c_bool_cnt(0),
8886
proper_bool_cnt(0),
8987
complex_cnt(0),
88+
bitint_cnt(0),
9089
int8_cnt(0),
9190
int16_cnt(0),
9291
int32_cnt(0),

0 commit comments

Comments
 (0)