Merge pull request #7684 from tautschnig/cleanup/remove-inhibit_unused_functions

Remove dfcc_utilst::inhibit_unused_functions

Author: tautschnig

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

@@ -513,7 +513,21 @@ void dfcct::transform_goto_model()
   instrument_other_functions();
   library.inhibit_front_end_builtins();
 
-  // TODO implement and use utils.inhibit_unreachable_functions(harness);
+  // TODO implement a means to inhibit unreachable functions (possibly via the
+  // code that implements drop-unused-functions followed by
+  // generate-function-bodies):
+  // Traverse 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
+  // functions that are not in the used function set into:
+  //  ```c
+  //  assert(false, "function identified as unreachable");
+  //  assume(false);
+  //  ```
+  // That way, if the analysis mistakenly pruned some functions, assertions
+  // will be violated and the analysis will fail.
+  // TODO: add a command line flag to tell the instrumentation to not prune
+  // a function.
   goto_model.goto_functions.update();
 
   remove_skip(goto_model);

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

@@ -552,8 +552,3 @@ void dfcc_utilst::inline_program(
     decorated.get_not_enough_arguments_set().end());
   goto_model.goto_functions.update();
 }
-
-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

@@ -223,21 +223,6 @@ class dfcc_utilst
     std::set<irep_idt> &recursive_call,
     std::set<irep_idt> &missing_function,
     std::set<irep_idt> &not_enough_arguments);
-
-  /// \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
-  /// functions that are not in the used function set into:
-  ///  ```c
-  ///  assert(false, "function identified as unreachable");
-  ///  assume(false);
-  ///  ```
-  /// That way, if the analysis mistakenly pruned some functions, assertions
-  /// will be violated and the analysis will fail.
-  /// TODO: add a command line flag to tell the instrumentation to not prune
-  /// a function.
-  /// \param start name of the entry point
-  void inhibit_unused_functions(const irep_idt &start);
 };
 
 #endif