Merge pull request #6493 from tautschnig/followup-6473

Invoke goto_functions.update() after inlining

Author: tautschnig

regression/contracts/invar_check_large/main.c

@@ -23,6 +23,7 @@ int main()
   int r = 1;
   while(h > l)
     // clang-format off
+    __CPROVER_assigns(arr0, arr1, arr2, arr3, arr4, h, l, r)
     __CPROVER_loop_invariant(
       // Turn off `clang-format` because it breaks the `==>` operator.
       h >= l &&
@@ -61,6 +62,11 @@ int main()
           r = h;
           l++;
         }
+        else
+        {
+          h--;
+          l++;
+        }
       }
       else if(*(arr[h]) <= pivot)
       {

regression/contracts/invar_check_large/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main.assertion.1\] .* assertion 0 <= r && r < 5: SUCCESS$
 ^\[main.assertion.2\] .* assertion \*\(arr\[r\]\) == pivot: SUCCESS$
 ^\[main.assertion.3\] .* assertion 0 < r ==> arr0 <= pivot: SUCCESS$

src/goto-instrument/contracts/contracts.cpp

@@ -773,10 +773,14 @@ void code_contractst::apply_loop_contract(
   const irep_idt &function_name,
   goto_functionst::goto_functiont &goto_function)
 {
-  local_may_aliast local_may_alias(goto_function);
-  natural_loops_mutablet natural_loops(goto_function.body);
-
-  if(!natural_loops.loop_map.size())
+  const bool may_have_loops = std::any_of(
+    goto_function.body.instructions.begin(),
+    goto_function.body.instructions.end(),
+    [](const goto_programt::instructiont &instruction) {
+      return instruction.is_backwards_goto();
+    });
+
+  if(!may_have_loops)
     return;
 
   inlining_decoratort decorated(log.get_message_handler());
@@ -787,6 +791,12 @@ void code_contractst::apply_loop_contract(
     decorated.get_recursive_function_warnings_count() == 0,
     "Recursive functions found during inlining");
 
+  // restore internal invariants
+  goto_functions.update();
+
+  local_may_aliast local_may_alias(goto_function);
+  natural_loops_mutablet natural_loops(goto_function.body);
+
   // A graph node type that stores information about a loop.
   // We create a DAG representing nesting of various loops in goto_function,
   // sort them topologically, and instrument them in the top-sorted order.