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

Author: tautschnig

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.

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();

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

@@ -265,14 +265,16 @@ 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,
     no_body,
     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)

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.