Skip to content

Commit cbba9f8

Browse files
kroeningkroening
committed
C23 keywords
This adds scanner, parser and typechecker support for the new C23 keywords.
1 parent b0457fa commit cbba9f8

10 files changed

+82
-37
lines changed

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

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

‎regression/ansi-c/constants/predefined-constants1.desc

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

‎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);

‎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);

‎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
}

‎src/ansi-c/parser.y

+34-2
Original file line numberDiff line numberDiff line change
@@ -62,8 +62,9 @@ int yyansi_cerror(const std::string &error);
6262

6363
%token TOK_AUTO "auto"
6464
%token TOK_BOOL "bool"
65-
%token TOK_COMPLEX "complex"
65+
%token TOK_BITINT "_BitInt"
6666
%token TOK_BREAK "break"
67+
%token TOK_COMPLEX "complex"
6768
%token TOK_CASE "case"
6869
%token TOK_CHAR "char"
6970
%token TOK_CONST "const"
@@ -91,6 +92,7 @@ int yyansi_cerror(const std::string &error);
9192
%token TOK_STRUCT "struct"
9293
%token TOK_SWITCH "switch"
9394
%token TOK_TYPEDEF "typedef"
95+
%token TOK_TYPEOF_UNQUAL "typeof_unqual"
9496
%token TOK_UNION "union"
9597
%token TOK_UNSIGNED "unsigned"
9698
%token TOK_VOID "void"
@@ -344,10 +346,30 @@ string:
344346

345347
/*** Constants **********************************************************/
346348

347-
constant: integer
349+
constant:
350+
integer
348351
| floating
349352
| character
350353
| string
354+
| predefined-constant
355+
;
356+
357+
predefined-constant:
358+
TOK_FALSE
359+
{ init($$, ID_constant);
360+
stack_expr($$).set(ID_value, ID_false);
361+
stack_expr($$).type() = bool_typet{};
362+
}
363+
| TOK_TRUE
364+
{ init($$, ID_constant);
365+
stack_expr($$).set(ID_value, ID_true);
366+
stack_expr($$).type() = bool_typet{};
367+
}
368+
| TOK_NULLPTR
369+
{ init($$, ID_constant);
370+
stack_expr($$).set(ID_value, ID_NULL);
371+
stack_expr($$).type() = pointer_type(void_type());
372+
}
351373
;
352374

353375
/*** Expressions ********************************************************/
@@ -1338,6 +1360,16 @@ typeof_specifier:
13381360
parser_stack($$).id(ID_typeof);
13391361
parser_stack($$).set(ID_type_arg, parser_stack($3));
13401362
}
1363+
| TOK_TYPEOF_UNQUAL '(' comma_expression ')'
1364+
{ $$ = $1;
1365+
parser_stack($$).id(ID_typeof_unqual);
1366+
mto($$, $3);
1367+
}
1368+
| TOK_TYPEOF_UNQUAL '(' type_name ')'
1369+
{ $$ = $1;
1370+
parser_stack($$).id(ID_typeof_unqual);
1371+
parser_stack($$).set(ID_type_arg, parser_stack($3));
1372+
}
13411373
;
13421374

13431375
typeof_type_specifier:

‎src/ansi-c/scanner.l

+17-32
Original file line numberDiff line numberDiff line change
@@ -162,28 +162,6 @@ int conditional_keyword(bool condition, int token)
162162
return make_identifier();
163163
}
164164

165-
int c17_keyword(int token)
166-
{
167-
if(PARSER.c17)
168-
{
169-
loc();
170-
return token;
171-
}
172-
else
173-
return make_identifier();
174-
}
175-
176-
int c23_keyword(int token)
177-
{
178-
if(PARSER.c23)
179-
{
180-
loc();
181-
return token;
182-
}
183-
else
184-
return make_identifier();
185-
}
186-
187165
int MSC_cpp_keyword(int token)
188166
{
189167
if(PARSER.cpp98 && PARSER.mode==configt::ansi_ct::flavourt::VISUAL_STUDIO)
@@ -852,15 +830,22 @@ enable_or_disable ("enable"|"disable")
852830
return make_identifier();
853831
}
854832

833+
%{
834+
/* C23 Keywords */
835+
%}
836+
837+
"_BitInt" { return conditional_keyword(PARSER.c23, TOK_BITINT); }
838+
"_typeof_unqual" { return conditional_keyword(PARSER.c23, TOK_TYPEOF_UNQUAL); }
839+
855840
%{
856841
/* C++ Keywords and Operators */
857842
%}
858843

859-
"alignas" { return conditional_keyword(PARSER.cpp11, TOK_ALIGNAS); } // C++11
860-
"alignof" { return conditional_keyword(PARSER.cpp11, TOK_ALIGNOF); } // C++11
844+
"alignas" { return conditional_keyword(PARSER.cpp11 || PARSER.c23, TOK_ALIGNAS); }
845+
"alignof" { return conditional_keyword(PARSER.cpp11 || PARSER.c23, TOK_ALIGNOF); }
861846
"and" { return conditional_keyword(PARSER.cpp98, TOK_ANDAND); }
862847
"and_eq" { return conditional_keyword(PARSER.cpp98, TOK_ANDASSIGN); }
863-
"bool" { return conditional_keyword(PARSER.cpp98, TOK_BOOL); }
848+
"bool" { return conditional_keyword(PARSER.cpp98 || PARSER.c23, TOK_BOOL); }
864849
"catch" { return conditional_keyword(PARSER.cpp98, TOK_CATCH); }
865850
"char16_t" { // C++11, but Visual Studio uses typedefs
866851
return conditional_keyword(
@@ -876,11 +861,11 @@ enable_or_disable ("enable"|"disable")
876861
}
877862
"class" { return conditional_keyword(PARSER.cpp98, TOK_CLASS); }
878863
"compl" { return conditional_keyword(PARSER.cpp98, '~'); }
879-
"constexpr" { return conditional_keyword(PARSER.cpp11, TOK_CONSTEXPR); } // C++11
864+
"constexpr" { return conditional_keyword(PARSER.cpp11 || PARSER.c23, TOK_CONSTEXPR); }
880865
"delete" { return conditional_keyword(PARSER.cpp98, TOK_DELETE); }
881866
"decltype" { return conditional_keyword(PARSER.cpp11, TOK_DECLTYPE); } // C++11
882867
"explicit" { return conditional_keyword(PARSER.cpp98, TOK_EXPLICIT); }
883-
"false" { return conditional_keyword(PARSER.cpp98, TOK_FALSE); }
868+
"false" { return conditional_keyword(PARSER.cpp98 || PARSER.c23, TOK_FALSE); }
884869
"friend" { return conditional_keyword(PARSER.cpp98, TOK_FRIEND); }
885870
"mutable" { return conditional_keyword(PARSER.cpp98, TOK_MUTABLE); }
886871
"namespace" { return conditional_keyword(PARSER.cpp98, TOK_NAMESPACE); }
@@ -890,7 +875,7 @@ enable_or_disable ("enable"|"disable")
890875
"noreturn" { return conditional_keyword(PARSER.cpp11, TOK_NORETURN); } // C++11
891876
"not" { return conditional_keyword(PARSER.cpp98, '!'); }
892877
"not_eq" { return conditional_keyword(PARSER.cpp98, TOK_NE); }
893-
"nullptr" { return conditional_keyword(PARSER.cpp11, TOK_NULLPTR); } // C++11
878+
"nullptr" { return conditional_keyword(PARSER.cpp11 || PARSER.c23, TOK_NULLPTR); }
894879
"operator" { return conditional_keyword(PARSER.cpp98, TOK_OPERATOR); }
895880
"or" { return conditional_keyword(PARSER.cpp98, TOK_OROR); }
896881
"or_eq" { return conditional_keyword(PARSER.cpp98, TOK_ORASSIGN); }
@@ -901,15 +886,15 @@ enable_or_disable ("enable"|"disable")
901886
// as a keyword, even though the documentation claims
902887
// it's a macro.
903888
return conditional_keyword(
904-
PARSER.cpp11 ||
889+
PARSER.cpp11 || PARSER.c23 ||
905890
PARSER.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO,
906891
TOK_STATIC_ASSERT);
907892
}
908893
"template" { return conditional_keyword(PARSER.cpp98, TOK_TEMPLATE); }
909894
"this" { return conditional_keyword(PARSER.cpp98, TOK_THIS); }
910-
"thread_local" { return conditional_keyword(PARSER.cpp11, TOK_THREAD_LOCAL); } // C++11
895+
"thread_local" { return conditional_keyword(PARSER.cpp11 || PARSER.c23, TOK_THREAD_LOCAL); }
911896
"throw" { return conditional_keyword(PARSER.cpp98, TOK_THROW); }
912-
"true" { return conditional_keyword(PARSER.cpp98, TOK_TRUE); }
897+
"true" { return conditional_keyword(PARSER.cpp98 || PARSER.c23, TOK_TRUE); }
913898
"typeid" { return conditional_keyword(PARSER.cpp98, TOK_TYPEID); }
914899
"typename" { return conditional_keyword(PARSER.cpp98, TOK_TYPENAME); }
915900
"using" { return conditional_keyword(PARSER.cpp98, TOK_USING); }
@@ -1241,7 +1226,7 @@ enable_or_disable ("enable"|"disable")
12411226
return make_identifier();
12421227
}
12431228

1244-
"typeof" { if(PARSER.cpp98 ||
1229+
"typeof" { if(PARSER.cpp98 || PARSER.c23 ||
12451230
PARSER.mode==configt::ansi_ct::flavourt::GCC ||
12461231
PARSER.mode==configt::ansi_ct::flavourt::CLANG ||
12471232
PARSER.mode==configt::ansi_ct::flavourt::CODEWARRIOR ||

‎src/util/config.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -1238,6 +1238,12 @@ bool configt::set(const cmdlinet &cmdline)
12381238
if(cmdline.isset("c11"))
12391239
ansi_c.set_c11();
12401240

1241+
if(cmdline.isset("c17"))
1242+
ansi_c.set_c17();
1243+
1244+
if(cmdline.isset("c23"))
1245+
ansi_c.set_c23();
1246+
12411247
if(cmdline.isset("cpp98"))
12421248
cpp.set_cpp98();
12431249

‎src/util/config.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ class symbol_table_baset;
2323

2424
#define OPT_CONFIG_C_CPP \
2525
"D:I:(include)(function)" \
26-
"(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
26+
"(c89)(c99)(c11)(c17)(c23)(cpp98)(cpp03)(cpp11)" \
2727
"(unsigned-char)" \
2828
"(round-to-even)(round-to-nearest)" \
2929
"(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \

‎src/util/irep_ids.def

+1
Original file line numberDiff line numberDiff line change
@@ -343,6 +343,7 @@ IREP_ID_ONE(gcc_local_label)
343343
IREP_ID_ONE(gcc)
344344
IREP_ID_ONE(msc)
345345
IREP_ID_ONE(typeof)
346+
IREP_ID_ONE(typeof_unqual)
346347
IREP_ID_ONE(ellipsis)
347348
IREP_ID_ONE(flavor)
348349
IREP_ID_TWO(ge, >=)

0 commit comments

Comments
 (0)