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

Author: tautschnig

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;
+}

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
+^EXIT=0$
+^SIGNAL=0$
+^WARNING: generate function bodies: Function\(s\) matched but already have bodies

regression/goto-instrument/generate-function-body-mixed/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+void generate_me();
+
+void already_has_body()
+{
+  assert(0);
+}
+
+int main(void)
+{
+  generate_me();
+  already_has_body();
+  return 0;
+}

regression/goto-instrument/generate-function-body-mixed/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--generate-function-body '.*' --generate-function-body-options assert-false
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[generate_me.assertion.1\] .* undefined function should be unreachable: FAILURE$

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;
+}

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
+^EXIT=0$
+^SIGNAL=0$
+^WARNING: generate function bodies: No function name matched regex

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;
+    }
   }
 }
 

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} <option> "                                     \
   "{ufun_name},{yparams}:{up1};{up2};.. \t "                                   \
   "generate havocing body\n"                                                   \