Merge pull request #7682 from tautschnig/cleanup/remove-dfcc-has_no_loops

Remove dfcc_utilst::has_no_loops

Author: tautschnig

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

@@ -64,7 +64,7 @@ void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions(
   // inline resulting program and check for loops
   inline_and_check_warnings(dest);
   PRECONDITION_WITH_DIAGNOSTICS(
-    utils.has_no_loops(dest),
+    is_loop_free(dest, ns, log),
     "loops in assigns clause specification functions must be unwound before "
     "contracts instrumentation");
 }
@@ -91,7 +91,7 @@ void dfcc_contract_clauses_codegent::gen_spec_frees_instructions(
   // inline resulting program and check for loops
   inline_and_check_warnings(dest);
   PRECONDITION_WITH_DIAGNOSTICS(
-    utils.has_no_loops(dest),
+    is_loop_free(dest, ns, log),
     "loops in assigns clause specification functions must be unwound before "
     "contracts instrumentation");
 }

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

@@ -553,17 +553,6 @@ void dfcc_utilst::inline_program(
   goto_model.goto_functions.update();
 }
 
-bool dfcc_utilst::has_no_loops(const goto_programt &goto_program)
-{
-  return is_loop_free(goto_program, ns, log);
-}
-
-bool dfcc_utilst::has_no_loops(const irep_idt &function_id)
-{
-  return has_no_loops(
-    goto_model.goto_functions.function_map.at(function_id).body);
-}
-
 void dfcc_utilst::inhibit_unused_functions(const irep_idt &start)
 {
   PRECONDITION_WITH_DIAGNOSTICS(false, "not yet implemented");

src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h

@@ -211,9 +211,6 @@ class dfcc_utilst
     std::set<irep_idt> &missing_function,
     std::set<irep_idt> &not_enough_arguments);
 
-  /// \returns True iff \p function_id is loop free.
-  bool has_no_loops(const irep_idt &function_id);
-
   /// \brief Inlines the given program, aborts on recursive calls during
   /// inlining.
   void inline_program(goto_programt &program);
@@ -227,9 +224,6 @@ class dfcc_utilst
     std::set<irep_idt> &missing_function,
     std::set<irep_idt> &not_enough_arguments);
 
-  /// \returns True iff \p goto_program is loop free.
-  bool has_no_loops(const goto_programt &goto_program);
-
   /// \brief Traverses the call tree from the given entry point to identify
   /// functions symbols that are effectively called in the model,
   /// Then goes over all functions of the model and turns the bodies of all