Skip to content

Commit 5a39bdd

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

25 files changed

+351
-80
lines changed

‎doc/man/cbmc.1‎

Lines changed: 1 addition & 1 deletion
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

‎regression/cbmc/_BitInt/_BitInt1.c‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// _BitInt is a C23 feature
2+
#include <assert.h>
3+
4+
int main()
5+
{
6+
// sizeof
7+
static_assert(sizeof(_BitInt(32)) == 4);
8+
static_assert(sizeof(_BitInt(33)) == 8);
9+
static_assert(sizeof(_BitInt(65)) == 16);
10+
static_assert(sizeof(_BitInt(128)) == 16);
11+
12+
// casts
13+
//assert((_BitInt(4))17 == 1);
14+
//assert((_BitInt(4)) - 1 == -1);
15+
//assert((unsigned _BitInt(4)) - 1 == 15);
16+
17+
// promotion (or lack thereof)
18+
//assert((unsigned _BitInt(4))15 + (unsigned _BitInt(4))1 == 0);
19+
// assert((unsigned _BitInt(4))15 + (unsigned _BitInt(5))1 == 16);
20+
//assert((unsigned _BitInt(4))15 + (signed _BitInt(5))1 == -16);
21+
// assert((unsigned _BitInt(4))15 + 1 == 16);
22+
23+
// pointers
24+
_BitInt(3) x, *p = &x;
25+
//*p = 1;
26+
27+
return 0;
28+
}

‎regression/cbmc/_BitInt/_BitInt1.desc‎

Lines changed: 8 additions & 0 deletions
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/constants/predefined-constants1.c‎

Lines changed: 10 additions & 0 deletions
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‎

Lines changed: 7 additions & 0 deletions
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‎

Lines changed: 17 additions & 0 deletions
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‎

Lines changed: 8 additions & 0 deletions
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‎

Lines changed: 23 additions & 0 deletions
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‎

Lines changed: 8 additions & 0 deletions
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‎

Lines changed: 42 additions & 29 deletions
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

0 commit comments

Comments
 (0)