From 5a1e105cf1c69b53f0e6527312c51a5c1f830334 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 30 Nov 2025 14:04:58 +0000 Subject: [PATCH] Fix misleading error message for --generate-function-body on existing bodies Previously, when the option was used with a function name that matched an existing function that already had a body, the error message incorrectly stated "No function name matched regex", which confused users into thinking their regex was wrong when in fact the function was found but had an existing body. The fix improves user experience by providing clear, actionable error messages that distinguish between: - Functions that don't match the provided regex - Functions that match the regex but already have bodies (and thus cannot have bodies generated) Fixes: #2974 --- .../main.c | 13 ++++++ .../test.desc | 6 +++ .../generate-function-body-mixed/main.c | 15 ++++++ .../generate-function-body-mixed/test.desc | 7 +++ .../generate-function-body-no-match/main.c | 10 ++++ .../generate-function-body-no-match/test.desc | 6 +++ .../generate_function_bodies.cpp | 46 +++++++++++++------ .../generate_function_bodies.h | 3 +- 8 files changed, 90 insertions(+), 16 deletions(-) create mode 100644 regression/goto-instrument/generate-function-body-existing-body/main.c create mode 100644 regression/goto-instrument/generate-function-body-existing-body/test.desc create mode 100644 regression/goto-instrument/generate-function-body-mixed/main.c create mode 100644 regression/goto-instrument/generate-function-body-mixed/test.desc create mode 100644 regression/goto-instrument/generate-function-body-no-match/main.c create mode 100644 regression/goto-instrument/generate-function-body-no-match/test.desc diff --git a/regression/goto-instrument/generate-function-body-existing-body/main.c b/regression/goto-instrument/generate-function-body-existing-body/main.c new file mode 100644 index 00000000000..81c7d4283af --- /dev/null +++ b/regression/goto-instrument/generate-function-body-existing-body/main.c @@ -0,0 +1,13 @@ +int generate_my_body(); + +int replace_my_body() +{ + return 1; +} + +int main(void) +{ + generate_my_body(); + replace_my_body(); + return 0; +} diff --git a/regression/goto-instrument/generate-function-body-existing-body/test.desc b/regression/goto-instrument/generate-function-body-existing-body/test.desc new file mode 100644 index 00000000000..4933822e059 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-existing-body/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--generate-function-body replace_my_body --generate-function-body-options assert-false +^generate function bodies: Function\(s\) matched but already have bodies +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/generate-function-body-mixed/main.c b/regression/goto-instrument/generate-function-body-mixed/main.c new file mode 100644 index 00000000000..ab46711eb0a --- /dev/null +++ b/regression/goto-instrument/generate-function-body-mixed/main.c @@ -0,0 +1,15 @@ +#include + +void generate_me(); + +void already_has_body() +{ + assert(0); +} + +int main(void) +{ + generate_me(); + already_has_body(); + return 0; +} diff --git a/regression/goto-instrument/generate-function-body-mixed/test.desc b/regression/goto-instrument/generate-function-body-mixed/test.desc new file mode 100644 index 00000000000..6d7785968d6 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-mixed/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--generate-function-body '[ag].*' --generate-function-body-options assert-false +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^\[generate_me.assertion.1\] .* undefined function should be unreachable: FAILURE$ diff --git a/regression/goto-instrument/generate-function-body-no-match/main.c b/regression/goto-instrument/generate-function-body-no-match/main.c new file mode 100644 index 00000000000..a9f4a190555 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-no-match/main.c @@ -0,0 +1,10 @@ +int some_function() +{ + return 1; +} + +int main(void) +{ + some_function(); + return 0; +} diff --git a/regression/goto-instrument/generate-function-body-no-match/test.desc b/regression/goto-instrument/generate-function-body-no-match/test.desc new file mode 100644 index 00000000000..676e236f83f --- /dev/null +++ b/regression/goto-instrument/generate-function-body-no-match/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--generate-function-body nonexistent_function --generate-function-body-options assert-false +^generate function bodies: No function name matched regex +^EXIT=0$ +^SIGNAL=0$ diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 7639ebe78e4..8212478f2a3 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -510,30 +510,46 @@ void generate_function_bodies( messaget messages(message_handler); const std::regex cprover_prefix = std::regex("__CPROVER.*"); bool did_generate_body = false; + bool matched_function_with_body = false; for(auto &function : model.goto_functions.function_map) { - if( - !function.second.body_available() && - std::regex_match(id2string(function.first), functions_regex)) + if(std::regex_match(id2string(function.first), functions_regex)) { - if(std::regex_match(id2string(function.first), cprover_prefix)) + if(!function.second.body_available()) { - messages.warning() << "generate function bodies: matched function '" - << id2string(function.first) - << "' begins with __CPROVER " - << "the generated body for this function " - << "may interfere with analysis" << messaget::eom; + if(std::regex_match(id2string(function.first), cprover_prefix)) + { + messages.warning() + << "generate function bodies: matched function '" + << id2string(function.first) << "' begins with __CPROVER " + << "the generated body for this function " + << "may interfere with analysis" << messaget::eom; + } + did_generate_body = true; + generate_function_body.generate_function_body( + function.second, model.symbol_table, function.first); + } + else + { + matched_function_with_body = true; } - did_generate_body = true; - generate_function_body.generate_function_body( - function.second, model.symbol_table, function.first); } } if(!did_generate_body && !ignore_no_match) { - messages.warning() - << "generate function bodies: No function name matched regex" - << messaget::eom; + if(matched_function_with_body) + { + messages.warning() + << "generate function bodies: Function(s) matched but already have " + << "bodies (body generation is only performed for functions without " + << "existing bodies)" << messaget::eom; + } + else + { + messages.warning() + << "generate function bodies: No function name matched regex" + << messaget::eom; + } } } diff --git a/src/goto-instrument/generate_function_bodies.h b/src/goto-instrument/generate_function_bodies.h index 7d1ed12266e..11014c7d06f 100644 --- a/src/goto-instrument/generate_function_bodies.h +++ b/src/goto-instrument/generate_function_bodies.h @@ -92,7 +92,8 @@ void generate_function_bodies( #define HELP_REPLACE_FUNCTION_BODY \ " {y--generate-function-body} {uregex} \t " \ - "generate bodies for functions matching {uregex}\n" \ + "generate bodies for functions matching {uregex} that do not already " \ + "have bodies\n" \ " {y--generate-havocing-body}