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

Diff for: ‎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

Diff for: ‎regression/cbmc/_BitInt/_BitInt1.c

+28
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+
}

Diff for: ‎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$

Diff for: ‎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+
}

Diff for: ‎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

Diff for: ‎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+
}

Diff for: ‎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$

Diff for: ‎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+
}

Diff for: ‎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$

Diff for: ‎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

Diff for: ‎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),

Diff for: ‎src/ansi-c/ansi_c_language.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,11 @@ bool ansi_c_languaget::parse(
8080
ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
8181
ansi_c_parser.cpp98=false; // it's not C++
8282
ansi_c_parser.cpp11=false; // it's not C++
83+
ansi_c_parser.c17 =
84+
config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C17 ||
85+
config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C23;
86+
ansi_c_parser.c23 =
87+
config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C23;
8388
ansi_c_parser.mode=config.ansi_c.mode;
8489

8590
ansi_c_scanner_init(ansi_c_parser);

Diff for: ‎src/ansi-c/builtin_factory.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,8 @@ static bool convert(
5858
ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
5959
ansi_c_parser.cpp98=false; // it's not C++
6060
ansi_c_parser.cpp11=false; // it's not C++
61+
ansi_c_parser.c17 = false; // we do C11 for now
62+
ansi_c_parser.c23 = false; // we do C11 for now
6163
ansi_c_parser.mode=config.ansi_c.mode;
6264

6365
ansi_c_scanner_init(ansi_c_parser);

Diff for: ‎src/ansi-c/c_preprocess.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -602,10 +602,10 @@ bool c_preprocess_gcc_clang(
602602
case configt::ansi_ct::c_standardt::C23:
603603
#if defined(__OpenBSD__)
604604
if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
605-
argv.push_back("-std=c23");
605+
argv.push_back("-std=c2x");
606606
else
607607
#endif
608-
argv.push_back("-std=gnu23");
608+
argv.push_back("-std=gnu2x");
609609
break;
610610
}
611611
}

Diff for: ‎src/ansi-c/c_typecheck_base.h

+1
Original file line numberDiff line numberDiff line change
@@ -265,6 +265,7 @@ class c_typecheck_baset:
265265
virtual void typecheck_array_type(array_typet &type);
266266
virtual void typecheck_vector_type(typet &type);
267267
virtual void typecheck_custom_type(typet &type);
268+
virtual void typecheck_bitint_type(typet &);
268269
virtual void adjust_function_parameter(typet &type) const;
269270
virtual bool is_complete_type(const typet &type) const;
270271

Diff for: ‎src/ansi-c/c_typecheck_code.cpp

+6-3
Original file line numberDiff line numberDiff line change
@@ -105,10 +105,13 @@ void c_typecheck_baset::typecheck_code(codet &code)
105105
}
106106
else if(statement==ID_static_assert)
107107
{
108-
PRECONDITION(code.operands().size() == 2);
108+
// C23 allows static_assert without message
109+
PRECONDITION(code.operands().size() == 1 || code.operands().size() == 2);
109110

110111
typecheck_expr(code.op0());
111-
typecheck_expr(code.op1());
112+
113+
if(code.operands().size() == 2)
114+
typecheck_expr(code.op1());
112115

113116
implicit_typecast_bool(code.op0());
114117
make_constant(code.op0());
@@ -118,7 +121,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
118121
// failed
119122
error().source_location = code.find_source_location();
120123
error() << "static assertion failed";
121-
if(code.op1().id() == ID_string_constant)
124+
if(code.operands().size() == 2 && code.op1().id() == ID_string_constant)
122125
error() << ": " << to_string_constant(code.op1()).value();
123126
error() << eom;
124127
throw 0;

0 commit comments

Comments
 (0)