From f5b557597f6ae3e53d3ae7ee742016b41934c3d7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jul 2025 08:59:15 +0000 Subject: [PATCH] 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. Resolves: #8638 --- src/goto-instrument/contracts/dynamic-frames/dfcc.cpp | 3 ++- src/goto-instrument/generate_function_bodies.cpp | 7 +++++-- src/goto-instrument/generate_function_bodies.h | 3 ++- src/goto-instrument/goto_instrument_parse_options.cpp | 6 ++++-- 4 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index cbc616f7aa9..1403b04f403 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -497,7 +497,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(); diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index bff129baa70..7639ebe78e4 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -498,11 +498,14 @@ std::unique_ptr 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" diff --git a/src/goto-instrument/generate_function_bodies.h b/src/goto-instrument/generate_function_bodies.h index 2f4cb2380c5..7d1ed12266e 100644 --- a/src/goto-instrument/generate_function_bodies.h +++ b/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. diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3b60d0fe95d..c13ffaec145 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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 {