Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions regression/ansi-c/gcc_nested_functions1/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
// Test basic nested function definition
int main()
{
int outer_var = 10;

// Nested function definition
int nested_func(int x)
{
return x + outer_var;
}

int result = nested_func(5);
__CPROVER_assert(
result == 15, "nested function should access outer variable");

return 0;
}
9 changes: 9 additions & 0 deletions regression/ansi-c/gcc_nested_functions1/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
^PARSING ERROR$
20 changes: 20 additions & 0 deletions regression/ansi-c/gcc_nested_functions2/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
// Test nested function with auto keyword and forward declaration
int main()
{
int outer_var = 20;

// Forward declaration with auto keyword
auto int nested_func(int x);

// Nested function definition
int nested_func(int x)
{
return x * outer_var;
}

int result = nested_func(3);
__CPROVER_assert(
result == 60, "nested function should access outer variable");

return 0;
}
9 changes: 9 additions & 0 deletions regression/ansi-c/gcc_nested_functions2/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
^PARSING ERROR$
23 changes: 23 additions & 0 deletions regression/ansi-c/gcc_nested_functions3/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
// Test multiple nested function calls and interactions
int main()
{
int base = 5;

int add(int x)
{
return x + base;
}

int multiply(int x)
{
return x * base;
}

int result1 = add(10);
int result2 = multiply(4);

__CPROVER_assert(result1 == 15, "add should work");
__CPROVER_assert(result2 == 20, "multiply should work");

return 0;
}
9 changes: 9 additions & 0 deletions regression/ansi-c/gcc_nested_functions3/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
^PARSING ERROR$
18 changes: 18 additions & 0 deletions regression/ansi-c/gcc_nested_functions4/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// Test taking address of nested function (if supported)
int main()
{
int multiplier = 3;

int multiply_by(int x)
{
return x * multiplier;
}

// Taking address of nested function
int (*func_ptr)(int) = multiply_by;

int result = func_ptr(7);
__CPROVER_assert(result == 21, "function pointer should work");

return 0;
}
9 changes: 9 additions & 0 deletions regression/ansi-c/gcc_nested_functions4/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
^PARSING ERROR$
35 changes: 35 additions & 0 deletions regression/cbmc/gcc_nested_functions/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
// GCC nested functions: verification of variable capture and calls
int main()
{
int outer = 10;

int add(int x)
{
return x + outer;
}

int multiply(int x)
{
return x * outer;
}

// basic call and variable capture
__CPROVER_assert(add(5) == 15, "add(5) == 15");
__CPROVER_assert(multiply(3) == 30, "multiply(3) == 30");

// mutation of captured variable is visible
outer = 20;
__CPROVER_assert(add(5) == 25, "add(5) == 25 after mutation");

// nested function used via function pointer
int (*fp)(int) = &add;
__CPROVER_assert(fp(1) == 21, "fp(1) == 21");

// nondet argument
int n;
__CPROVER_assume(n >= 0 && n <= 100);
int r = add(n);
__CPROVER_assert(r >= 20 && r <= 120, "add(n) in range");

return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/gcc_nested_functions/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
75 changes: 75 additions & 0 deletions src/ansi-c/parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -2360,6 +2360,7 @@ statement:
declaration_statement
| statement_attribute
| stmt_not_decl_or_attr
| gcc_nested_function_definition
;

stmt_not_decl_or_attr:
Expand All @@ -2385,6 +2386,80 @@ declaration_statement:
}
;

gcc_nested_function_definition:
declaration_specifier declarator
post_declarator_attributes_opt
Comment on lines +2389 to +2391
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

gcc_nested_function_definition only covers the declaration_specifier ... and type_specifier ... forms, but function_head supports additional GNU/C89-style heads (e.g., implicit-int identifier_declarator, and qualifier-only forms like declaration_qualifier_list identifier_declarator). As a result, some function heads accepted at top level won’t be accepted for nested definitions. Suggestion: mirror function_head’s alternatives here (or reuse/abstract the common function-head parsing) to avoid a feature gap and future divergence.

Copilot uses AI. Check for mistakes.
{
// This is a GCC nested function definition.
// We parse it like a top-level function_head.
$2=merge($3, $2);
init($$, ID_declaration);
parser_stack($$).type().swap(parser_stack($1));
PARSER.add_declarator(parser_stack($$), parser_stack($2));
// add_declarator forces functions to root scope; fix the name
// to use the current (local) scope prefix instead.
ansi_c_declaratort &d=
to_ansi_c_declaration(parser_stack($$)).declarator();
irep_idt base=d.get_base_name();
irep_idt local_name=
PARSER.current_scope().prefix+id2string(base);
d.set_name(local_name);
// Update scope entries so the name resolves locally.
PARSER.current_scope().name_map[base].prefixed_name=local_name;
PARSER.root_scope().name_map.erase(base);
create_function_scope($$);
Comment on lines +2398 to +2410
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

add_declarator writes function entries into root_scope().name_map[base] (and overwrites any existing mapping for the same base name) before this rule rewrites the declarator name. The subsequent root_scope().name_map.erase(base) will then remove the (possibly pre-existing) global mapping entirely, breaking later lookups of a global symbol with the same base name. Suggestion: avoid touching the root scope at all for nested function definitions (e.g., add a parser helper that adds a code declarator to the current scope), or at minimum snapshot any existing root_scope().name_map[base] entry before add_declarator and restore it afterwards (only erasing if it did not exist).

Copilot uses AI. Check for mistakes.
}
function_body
{
// Attach the body as the initializer, same as function_definition.
ansi_c_declarationt &ansi_c_declaration=
to_ansi_c_declaration(parser_stack($4));
INVARIANT(
ansi_c_declaration.declarators().size()==1,
"exactly one declarator");
ansi_c_declaration.add_initializer(parser_stack($5));
PARSER.pop_scope();
PARSER.clear_function();

Comment on lines +2420 to +2423
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

PARSER.clear_function() here clears the enclosing function context after finishing the nested function, but parsing then continues inside the outer function body. This can cause subsequent AST nodes in the outer function to lose their source_location.function, impacting things like __func__ expansion and any logic that relies on the function field for local scoping/name generation. Suggestion: restore the previous function identifier after pop_scope() instead of clearing it (e.g., maintain a small function-name stack in the parser, or capture the old function id before create_function_scope and reinstate it after the nested body).

Copilot uses AI. Check for mistakes.
// Wrap as a declaration statement so it fits in a block.
init($$);
statement($$, ID_decl);
mto($$, $4);
}
| type_specifier declarator
post_declarator_attributes_opt
{
$2=merge($3, $2);
init($$, ID_declaration);
parser_stack($$).type().swap(parser_stack($1));
PARSER.add_declarator(parser_stack($$), parser_stack($2));
ansi_c_declaratort &d=
to_ansi_c_declaration(parser_stack($$)).declarator();
irep_idt base=d.get_base_name();
irep_idt local_name=
PARSER.current_scope().prefix+id2string(base);
d.set_name(local_name);
PARSER.current_scope().name_map[base].prefixed_name=local_name;
PARSER.root_scope().name_map.erase(base);
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same root-scope clobbering issue as in the first alternative: add_declarator updates root_scope().name_map[base], and the later erase(base) can delete a pre-existing global mapping for that base name. Suggestion: keep nested function definitions entirely in the current scope (or save/restore any prior root-scope entry rather than unconditionally erasing).

Suggested change
PARSER.root_scope().name_map.erase(base);

Copilot uses AI. Check for mistakes.
create_function_scope($$);
}
function_body
{
ansi_c_declarationt &ansi_c_declaration=
to_ansi_c_declaration(parser_stack($4));
INVARIANT(
ansi_c_declaration.declarators().size()==1,
"exactly one declarator");
ansi_c_declaration.add_initializer(parser_stack($5));
PARSER.pop_scope();
PARSER.clear_function();

Comment on lines +2453 to +2456
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same outer-function context issue as above: clearing the parser's current function after a nested definition drops source_location.function for the remainder of the enclosing function body. This should restore the previous function id instead of clearing it.

Copilot uses AI. Check for mistakes.
init($$);
statement($$, ID_decl);
mto($$, $4);
}
;

gcc_attribute_specifier_opt:
/* empty */
{
Expand Down
Loading