Fix misleading error message for --generate-function-body on existing bodies

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

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 '[ag].*' --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
+^generate function bodies: No function name matched regex
+^EXIT=0$
+^SIGNAL=0$

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"                                                   \