From 79171e03d0765e0418e885808038feafc7187cd5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 17:45:35 +0100 Subject: [PATCH] C front-end: reject invalid array declarators - Reject VLA declarators with * outside function definitions - Reject type qualifiers and storage class specifiers in array declarators outside function prototypes According to the C standard (C99/C11): - Variable length array declarators with * are only valid in function parameter declarations within function definitions (not declarations) - Type qualifiers (like restrict, const, volatile) in array declarators are only valid in function parameter declarations - Storage class specifiers (like static) in array declarators are only valid in function parameter declarations within function prototypes or definitions These constructs are not valid in: - File scope variable declarations - Block scope variable declarations - Any array declarator in non-parameter contexts Fixes: #132 --- regression/ansi-c/Array_Declarator2/test.desc | 2 +- regression/ansi-c/Array_Declarator3/test.desc | 2 +- regression/ansi-c/Array_Declarator4/test.desc | 2 +- regression/ansi-c/Array_Declarator5/test.desc | 2 +- regression/ansi-c/Array_Declarator6/test.desc | 2 +- regression/ansi-c/Array_Declarator7/test.desc | 2 +- src/ansi-c/c_typecheck_base.cpp | 19 ++++ src/ansi-c/parser.y | 96 ++++++++++++++++++- 8 files changed, 120 insertions(+), 7 deletions(-) diff --git a/regression/ansi-c/Array_Declarator2/test.desc b/regression/ansi-c/Array_Declarator2/test.desc index bf5b3279b2c..c9e5d1c95cb 100644 --- a/regression/ansi-c/Array_Declarator2/test.desc +++ b/regression/ansi-c/Array_Declarator2/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=6$ diff --git a/regression/ansi-c/Array_Declarator3/test.desc b/regression/ansi-c/Array_Declarator3/test.desc index bf5b3279b2c..c9e5d1c95cb 100644 --- a/regression/ansi-c/Array_Declarator3/test.desc +++ b/regression/ansi-c/Array_Declarator3/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=6$ diff --git a/regression/ansi-c/Array_Declarator4/test.desc b/regression/ansi-c/Array_Declarator4/test.desc index bf5b3279b2c..c9e5d1c95cb 100644 --- a/regression/ansi-c/Array_Declarator4/test.desc +++ b/regression/ansi-c/Array_Declarator4/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=6$ diff --git a/regression/ansi-c/Array_Declarator5/test.desc b/regression/ansi-c/Array_Declarator5/test.desc index bf5b3279b2c..c9e5d1c95cb 100644 --- a/regression/ansi-c/Array_Declarator5/test.desc +++ b/regression/ansi-c/Array_Declarator5/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=6$ diff --git a/regression/ansi-c/Array_Declarator6/test.desc b/regression/ansi-c/Array_Declarator6/test.desc index 8f1b5f3a0e7..3bf3dd81863 100644 --- a/regression/ansi-c/Array_Declarator6/test.desc +++ b/regression/ansi-c/Array_Declarator6/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=6$ diff --git a/regression/ansi-c/Array_Declarator7/test.desc b/regression/ansi-c/Array_Declarator7/test.desc index b9d19b573eb..059be2cf96f 100644 --- a/regression/ansi-c/Array_Declarator7/test.desc +++ b/regression/ansi-c/Array_Declarator7/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=64$ diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index de4db8e8ef5..07a60110d6e 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -618,6 +618,25 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol) code_typet &code_type = to_code_type(symbol.type); + // Check for VLA unspecified ([*]) in function definitions + // This is only allowed in function prototypes, not definitions + for(const auto ¶m : code_type.parameters()) + { + typet t = param.type(); + while(t.id() == ID_array) + { + const array_typet &array_type = to_array_type(t); + if(array_type.get_bool(ID_C_vla_unspecified)) + { + error().source_location = param.source_location(); + error() << "'[*]' not allowed in other than function prototype scope" + << eom; + throw 0; + } + t = array_type.element_type(); + } + } + // reset labels labels_used.clear(); labels_defined.clear(); diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 91526b2b8e6..ee5ddcfba94 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -3532,7 +3532,73 @@ cprover_function_contract_sequence_opt: ; postfixing_abstract_declarator: - parameter_postfixing_abstract_declarator + non_parameter_array_abstract_declarator + | '(' ')' + { + // Set function name (last declarator) in source location + // before parsing function contracts. Only do this if we + // are at a global scope. + if (PARSER.current_scope().prefix.empty()) { + PARSER.set_function(PARSER.current_scope().last_declarator); + } + // Use last declarator (i.e., function name) to name + // the scope. + PARSER.new_scope( + id2string(PARSER.current_scope().last_declarator)+"::"); + } + cprover_function_contract_sequence_opt + { + set($1, ID_code); + stack_type($1).add(ID_parameters); + stack_type($1).add_subtype()=typet(ID_abstract); + PARSER.pop_scope(); + + // Clear function name in source location after parsing if + // at global scope. + if (PARSER.current_scope().prefix.empty()) { + PARSER.set_function(irep_idt()); + } + + $$ = merge($4, $1); + } + | '(' + { + // Set function name (last declarator) in source location + // before parsing function contracts. Only do this if we + // are at a global scope. + if (PARSER.current_scope().prefix.empty()) { + PARSER.set_function(PARSER.current_scope().last_declarator); + } + // Use last declarator (i.e., function name) to name + // the scope. + PARSER.new_scope( + id2string(PARSER.current_scope().last_declarator)+"::"); + } + parameter_type_list + ')' + KnR_parameter_header_opt + cprover_function_contract_sequence_opt + { + set($1, ID_code); + stack_type($1).add_subtype()=typet(ID_abstract); + stack_type($1).add(ID_parameters).get_sub(). + swap((irept::subt &)(to_type_with_subtypes(stack_type($3)).subtypes())); + PARSER.pop_scope(); + + // Clear function name in source location after parsing if + // at global scope. + if (PARSER.current_scope().prefix.empty()) { + PARSER.set_function(irep_idt()); + } + + if(parser_stack($5).is_not_nil()) + { + adjust_KnR_parameters(parser_stack($$).add(ID_parameters), parser_stack($5)); + parser_stack($$).set(ID_C_KnR, true); + } + + $$ = merge($6, $1); + } /* The following two rules implement K&R headers! */ | '(' ')' @@ -3636,6 +3702,32 @@ parameter_postfixing_abstract_declarator: } ; +non_parameter_array_abstract_declarator: + '[' ']' + { + $$=$1; + set($$, ID_array); + stack_type($$).add_subtype()=typet(ID_abstract); + stack_type($$).add(ID_size).make_nil(); + } + | '[' constant_expression ']' + { + $$=$1; + set($$, ID_array); + stack_type($$).add(ID_size).swap(parser_stack($2)); + stack_type($$).add_subtype()=typet(ID_abstract); + } + | non_parameter_array_abstract_declarator '[' constant_expression ']' + { + // we need to push this down + $$=$1; + set($2, ID_array); + stack_type($2).add(ID_size).swap(parser_stack($3)); + stack_type($2).add_subtype()=typet(ID_abstract); + make_subtype($1, $2); + } + ; + array_abstract_declarator: '[' ']' { @@ -3661,6 +3753,7 @@ array_abstract_declarator: set($$, ID_array); stack_type($$).add_subtype()=typet(ID_abstract); stack_type($$).add(ID_size).make_nil(); + stack_type($$).set(ID_C_vla_unspecified, true); } | '[' constant_expression ']' { @@ -3695,6 +3788,7 @@ array_abstract_declarator: set($2, ID_array); stack_type($2).add(ID_size).make_nil(); stack_type($2).add_subtype()=typet(ID_abstract); + stack_type($2).set(ID_C_vla_unspecified, true); make_subtype($1, $2); } ;