From 6356953829d9b4545cb4bbd6ad4c1676d3309ed5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Jul 2025 12:32:49 +0000
Subject: [PATCH] Contracts instrumentation: hide unhelpful "no body" warnings

Contracts instrumentation using inlining and has facilities to inspect
warnings to ensure no unexpected warnings arise. The expected ones,
however, should not be forwarded to the user as they cannot do anything
about them.

Closes: #8639
---
 .../contracts-dfcc/loop_assigns-slice-upto-fail/test.desc  | 1 +
 .../contracts/variant_multidimensional_ackermann/loop.desc | 2 +-
 src/goto-instrument/contracts/contracts.cpp                | 7 ++-----
 .../dynamic-frames/dfcc_contract_clauses_codegen.cpp       | 4 +++-
 .../contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp   | 6 ++++--
 5 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc b/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc
index 897a3670bfb..022e6e3d98c 100644
--- a/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc
+++ b/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc
@@ -19,5 +19,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 --
+no body for function '__CPROVER
 --
 This test shows that __CPROVER_object_upto is supported in loop contracts.
diff --git a/regression/contracts/variant_multidimensional_ackermann/loop.desc b/regression/contracts/variant_multidimensional_ackermann/loop.desc
index 82af4451f1a..eb904a6431d 100644
--- a/regression/contracts/variant_multidimensional_ackermann/loop.desc
+++ b/regression/contracts/variant_multidimensional_ackermann/loop.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-loop-contracts
 ^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 8cb69c96ed8..da25c01f569 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -848,12 +848,9 @@ void code_contractst::apply_loop_contract(
     return;
 
   inlining_decoratort decorated(log.get_message_handler());
-  goto_function_inline(
-    goto_functions, function_name, ns, log.get_message_handler());
+  goto_function_inline(goto_functions, function_name, ns, decorated);
 
-  INVARIANT(
-    decorated.get_recursive_call_set().size() == 0,
-    "Recursive functions found during inlining");
+  decorated.throw_on_recursive_calls(log, 0);
 
   // restore internal invariants
   goto_functions.update();
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
index 072e20b8efe..6c1d6d23fd0 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
@@ -265,6 +265,8 @@ void dfcc_contract_clauses_codegent::inline_and_check_warnings(
   std::set<irep_idt> recursive_call;
   std::set<irep_idt> not_enough_arguments;
 
+  // we inspect all warnings ourselves, no need to surface them
+  null_message_handlert null_message_handler;
   dfcc_utilst::inline_program(
     goto_model,
     goto_program,
@@ -272,7 +274,7 @@ void dfcc_contract_clauses_codegent::inline_and_check_warnings(
     recursive_call,
     missing_function,
     not_enough_arguments,
-    message_handler);
+    null_message_handler);
 
   // check that the only no body / missing functions are the cprover builtins
   for(const auto &id : no_body)
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
index 36c724498e2..c83a378d65e 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
@@ -339,9 +339,11 @@ void dfcc_infer_loop_assigns_for_function(
   auto malloc_body = goto_functions.function_map.extract(irep_idt("malloc"));
   auto free_body = goto_functions.function_map.extract(irep_idt("free"));
 
-  // Inline all function calls in goto_function_copy.
+  // Inline all function calls in goto_function_copy; this is best-effort
+  // inlining, we can safely ignore warnings here.
+  null_message_handlert null_message_handler;
   goto_program_inline(
-    goto_functions, goto_function_copy.body, ns, log.get_message_handler());
+    goto_functions, goto_function_copy.body, ns, null_message_handler);
   // Update the body to make sure all goto correctly jump to valid targets.
   goto_function_copy.body.update();
   // Build the loop graph after inlining.