DFCC: do not surface confusing warning

Users do not know that DFCC uses generate-function-bodies to ensure
sound operation, and indeed the user had everything set up just right
when _no_ function needed to be generated.

Towards: #8638

Author: tautschnig

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -518,7 +518,8 @@ void dfcct::transform_goto_model()
     std::regex("(?!" CPROVER_PREFIX ").*"),
     *generate_implementation,
     goto_model,
-    message_handler);
+    message_handler,
+    true);
   goto_model.goto_functions.update();
 
   reinitialize_model();

src/goto-instrument/generate_function_bodies.cpp

@@ -498,11 +498,14 @@ std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
 /// \param generate_function_body: Specifies what kind of body to generate
 /// \param model: The goto-model in which to generate the function bodies
 /// \param message_handler: Destination for status/warning messages
+/// \param ignore_no_match: Do not warn in case no function matched
+///   \p functions_regex
 void generate_function_bodies(
   const std::regex &functions_regex,
   const generate_function_bodiest &generate_function_body,
   goto_modelt &model,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  bool ignore_no_match)
 {
   messaget messages(message_handler);
   const std::regex cprover_prefix = std::regex("__CPROVER.*");
@@ -526,7 +529,7 @@ void generate_function_bodies(
         function.second, model.symbol_table, function.first);
     }
   }
-  if(!did_generate_body)
+  if(!did_generate_body && !ignore_no_match)
   {
     messages.warning()
       << "generate function bodies: No function name matched regex"

src/goto-instrument/generate_function_bodies.h

@@ -68,7 +68,8 @@ void generate_function_bodies(
   const std::regex &functions_regex,
   const generate_function_bodiest &generate_function_body,
   goto_modelt &model,
-  message_handlert &message_handler);
+  message_handlert &message_handler,
+  bool ignore_no_match);
 
 /// Generate a clone of \p function_name (labelled with \p call_site_id) and
 ///   instantiate its body with selective havocing of its parameters.

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1400,7 +1400,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       std::regex(cmdline.get_value("generate-function-body")),
       *generate_implementation,
       goto_model,
-      ui_message_handler);
+      ui_message_handler,
+      false);
   }
 
   if(cmdline.isset("generate-havocing-body"))
@@ -1427,7 +1428,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         std::regex(options_split[0]),
         *generate_implementation,
         goto_model,
-        ui_message_handler);
+        ui_message_handler,
+        false);
     }
     else
     {