Merge pull request #7681 from tautschnig/cleanup/remove-dfcc-set_hide

Replace DFCC's set_hide by call to make_hidden

Author: tautschnig

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

@@ -360,7 +360,8 @@ void dfcc_libraryt::load(std::set<irep_idt> &to_instrument)
   inline_functions();
 
   // hide all instructions in counter example traces
-  set_hide(true);
+  for(auto it : dfcc_fun_symbol)
+    goto_model.goto_functions.function_map.at(it.second.name).make_hidden();
 }
 
 optionalt<dfcc_funt> dfcc_libraryt::get_dfcc_fun(const irep_idt &id) const
@@ -512,14 +513,6 @@ void dfcc_libraryt::inhibit_front_end_builtins()
   }
 }
 
-/// Sets the given hide flag on all instructions of all library functions
-void dfcc_libraryt::set_hide(bool hide)
-{
-  PRECONDITION(dfcc_libraryt::loaded);
-  for(auto it : dfcc_fun_symbol)
-    utils.set_hide(it.second.name, hide);
-}
-
 const symbolt &dfcc_libraryt::get_instrumented_functions_map_symbol()
 {
   const irep_idt map_name = "__dfcc_instrumented_functions";

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

@@ -250,9 +250,6 @@ class dfcc_libraryt
   /// implementation.
   void inhibit_front_end_builtins();
 
-  /// Sets the given hide flag on all instructions of all library functions
-  void set_hide(bool hide);
-
   /// Adds "checked" pragmas to instructions of all library functions
   /// instructions. By default checks are not disabled.
   void disable_checks();

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

@@ -136,7 +136,7 @@ void dfcc_spec_functionst::generate_havoc_function(
     not_enough_arguments.empty(),
     "not enough arguments when inlining " + id2string(havoc_function_id));
 
-  utils.set_hide(havoc_function_id, true);
+  goto_model.goto_functions.function_map.at(havoc_function_id).make_hidden();
 
   goto_model.goto_functions.update();
 }
@@ -278,7 +278,7 @@ void dfcc_spec_functionst::to_spec_assigns_function(
   INVARIANT(
     function_pointer_contracts.empty(),
     "discovered function pointer contracts unexpectedly");
-  utils.set_hide(function_id, true);
+  goto_model.goto_functions.function_map.at(function_id).make_hidden();
 }
 
 void dfcc_spec_functionst::to_spec_assigns_instructions(
@@ -367,8 +367,7 @@ void dfcc_spec_functionst::to_spec_frees_function(
   INVARIANT(
     function_pointer_contracts.empty(),
     "discovered function pointer contracts unexpectedly");
-
-  utils.set_hide(function_id, true);
+  goto_model.goto_functions.function_map.at(function_id).make_hidden();
 }
 
 void dfcc_spec_functionst::to_spec_frees_instructions(

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

@@ -267,7 +267,7 @@ void dfcc_swap_and_wrapt::check_contract(
   // extend the signature of the wrapper function with the write set parameter
   utils.add_parameter(write_set_symbol, function_id);
 
-  utils.set_hide(wrapper_id, true);
+  goto_model.goto_functions.function_map.at(wrapper_id).make_hidden();
 
   // instrument the wrapped function
   instrument.instrument_wrapped_function(
@@ -305,7 +305,7 @@ void dfcc_swap_and_wrapt::replace_with_contract(
   body.add(goto_programt::make_end_function(
     utils.get_function_symbol(wrapper_id).location));
 
-  utils.set_hide(wrapper_id, true);
+  goto_model.goto_functions.function_map.at(wrapper_id).make_hidden();
 
   // write the body to the GOTO function
   goto_model.goto_functions.function_map.at(function_id).body.swap(body);

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

@@ -564,18 +564,6 @@ bool dfcc_utilst::has_no_loops(const irep_idt &function_id)
     goto_model.goto_functions.function_map.at(function_id).body);
 }
 
-void dfcc_utilst::set_hide(const irep_idt &function_id, bool hide)
-{
-  auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
-  if(goto_function.body_available())
-  {
-    Forall_goto_program_instructions(inst, goto_function.body)
-    {
-      inst->source_location_nonconst().set(ID_hide, hide);
-    }
-  }
-}
-
 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

@@ -230,10 +230,6 @@ class dfcc_utilst
   /// \returns True iff \p goto_program is loop free.
   bool has_no_loops(const goto_programt &goto_program);
 
-  /// \brief Sets the given hide flag on all instructions of the function if it
-  /// exists.
-  void set_hide(const irep_idt &function_id, bool hide);
-
   /// \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