Merge pull request #8697 from tautschnig/contracts-inlining-warnings

Contracts instrumentation: hide unhelpful "no body" warnings

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.

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$

src/goto-instrument/contracts/contracts.cpp

@@ -838,12 +838,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

@@ -336,9 +336,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.