Remove dfcc_utilst::inhibit_unused_functions

This has neither been implemented nor used so far. If a future use is
necessary, then this commit could be reverted, or the solution be
implemented in place (comment has now been moved to the only site that
intended to use it).

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