From b657866e9f9871c45beee280d61811503afca5a4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jun 2026 11:24:30 +0000 Subject: [PATCH] ansi-c: support qualified __auto_type GCC allows __auto_type with type qualifiers, e.g. const __auto_type x = init; which is equivalent to const typeof(init) x = init; The parser only had a production for the unqualified '__auto_type var = init;' form, so a qualified __auto_type -- as used by the Linux 6.12 kernel in arch/x86/include/asm/string_64.h -- failed with a syntax error. Add a declaring_list production for type_qualifier_list TOK_GCC_AUTO_TYPE declarator post_declarator_attributes_opt '=' initializer whose semantic action builds the typeof-of-initializer node and merges the qualifier list into it, mirroring GCC's documented semantics. Co-authored-by: Kiro --- regression/cbmc/auto_type_qualified/main.c | 11 ++++++++++ regression/cbmc/auto_type_qualified/test.desc | 10 ++++++++++ src/ansi-c/parser.y | 20 +++++++++++++++++++ 3 files changed, 41 insertions(+) create mode 100644 regression/cbmc/auto_type_qualified/main.c create mode 100644 regression/cbmc/auto_type_qualified/test.desc diff --git a/regression/cbmc/auto_type_qualified/main.c b/regression/cbmc/auto_type_qualified/main.c new file mode 100644 index 00000000000..60a441607ee --- /dev/null +++ b/regression/cbmc/auto_type_qualified/main.c @@ -0,0 +1,11 @@ +int main() +{ + int s = 42; + // 'const __auto_type x = s;' is equivalent to 'const typeof(s) x = s;'. + // The parser previously only handled the unqualified + // '__auto_type x = s;' form and rejected the qualified one. + const __auto_type x = s; + __CPROVER_assert( + x == 42, "qualified __auto_type deduces the initializer type"); + return 0; +} diff --git a/regression/cbmc/auto_type_qualified/test.desc b/regression/cbmc/auto_type_qualified/test.desc new file mode 100644 index 00000000000..4e93cfa3763 --- /dev/null +++ b/regression/cbmc/auto_type_qualified/test.desc @@ -0,0 +1,10 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +^PARSING ERROR$ +^syntax error diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 91526b2b8e6..c51a7f1c3dd 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -1114,6 +1114,26 @@ declaring_list: // add the initializer to_ansi_c_declaration(parser_stack($$)).add_initializer(parser_stack($5)); } + | type_qualifier_list TOK_GCC_AUTO_TYPE declarator + post_declarator_attributes_opt '=' initializer + { + // Qualified __auto_type: 'const/volatile/... __auto_type + // var = initializer;' is equivalent to + // ' typeof(initializer) var = initializer;'. + // Build the typeof-of-initializer node, then wrap it with + // the qualifiers. + parser_stack($2).id(ID_typeof); + parser_stack($2).copy_to_operands(parser_stack($6)); + // Merge qualifiers into the typeof type. + $2 = merge($1, $2); + + $3 = merge($4, $3); + + init($$, ID_declaration); + parser_stack($$).type().swap(parser_stack($2)); + PARSER.add_declarator(parser_stack($$), parser_stack($3)); + to_ansi_c_declaration(parser_stack($$)).add_initializer(parser_stack($6)); + } | declaring_list ',' gcc_type_attribute_opt declarator post_declarator_attributes_opt {