diff --git a/regression/ansi-c/gcc_nested_functions1/main.c b/regression/ansi-c/gcc_nested_functions1/main.c new file mode 100644 index 00000000000..8b8688773f5 --- /dev/null +++ b/regression/ansi-c/gcc_nested_functions1/main.c @@ -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; +} diff --git a/regression/ansi-c/gcc_nested_functions1/test.desc b/regression/ansi-c/gcc_nested_functions1/test.desc new file mode 100644 index 00000000000..77585324362 --- /dev/null +++ b/regression/ansi-c/gcc_nested_functions1/test.desc @@ -0,0 +1,9 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ +^PARSING ERROR$ diff --git a/regression/ansi-c/gcc_nested_functions2/main.c b/regression/ansi-c/gcc_nested_functions2/main.c new file mode 100644 index 00000000000..fa1666e4777 --- /dev/null +++ b/regression/ansi-c/gcc_nested_functions2/main.c @@ -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; +} diff --git a/regression/ansi-c/gcc_nested_functions2/test.desc b/regression/ansi-c/gcc_nested_functions2/test.desc new file mode 100644 index 00000000000..77585324362 --- /dev/null +++ b/regression/ansi-c/gcc_nested_functions2/test.desc @@ -0,0 +1,9 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ +^PARSING ERROR$ diff --git a/regression/ansi-c/gcc_nested_functions3/main.c b/regression/ansi-c/gcc_nested_functions3/main.c new file mode 100644 index 00000000000..4d05bc27561 --- /dev/null +++ b/regression/ansi-c/gcc_nested_functions3/main.c @@ -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; +} diff --git a/regression/ansi-c/gcc_nested_functions3/test.desc b/regression/ansi-c/gcc_nested_functions3/test.desc new file mode 100644 index 00000000000..77585324362 --- /dev/null +++ b/regression/ansi-c/gcc_nested_functions3/test.desc @@ -0,0 +1,9 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ +^PARSING ERROR$ diff --git a/regression/ansi-c/gcc_nested_functions4/main.c b/regression/ansi-c/gcc_nested_functions4/main.c new file mode 100644 index 00000000000..4c3310342bb --- /dev/null +++ b/regression/ansi-c/gcc_nested_functions4/main.c @@ -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; +} diff --git a/regression/ansi-c/gcc_nested_functions4/test.desc b/regression/ansi-c/gcc_nested_functions4/test.desc new file mode 100644 index 00000000000..77585324362 --- /dev/null +++ b/regression/ansi-c/gcc_nested_functions4/test.desc @@ -0,0 +1,9 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ +^PARSING ERROR$ diff --git a/regression/cbmc/gcc_nested_functions/main.c b/regression/cbmc/gcc_nested_functions/main.c new file mode 100644 index 00000000000..3f19361b513 --- /dev/null +++ b/regression/cbmc/gcc_nested_functions/main.c @@ -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; +} diff --git a/regression/cbmc/gcc_nested_functions/test.desc b/regression/cbmc/gcc_nested_functions/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/gcc_nested_functions/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 91526b2b8e6..1e48eb6be41 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -2360,6 +2360,7 @@ statement: declaration_statement | statement_attribute | stmt_not_decl_or_attr + | gcc_nested_function_definition ; stmt_not_decl_or_attr: @@ -2385,6 +2386,80 @@ declaration_statement: } ; +gcc_nested_function_definition: + declaration_specifier declarator + post_declarator_attributes_opt + { + // 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($$); + } + 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(); + + // 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); + 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(); + + init($$); + statement($$, ID_decl); + mto($$, $4); + } + ; + gcc_attribute_specifier_opt: /* empty */ {