Revert "Store "is hidden" attribute of goto functions in the symbol table"

This reverts commit ebfab8d.

Author: tautschnig

src/goto-instrument/cover_filter.cpp

@@ -29,7 +29,7 @@ bool internal_functions_filtert::operator()(
   if(function.name == INITIALIZE_FUNCTION)
     return false;
 
-  if(function.is_hidden())
+  if(goto_function.is_hidden())
     return false;
 
   // ignore Java built-ins (synthetic functions)

src/goto-programs/goto_convert_functions.cpp

@@ -226,10 +226,7 @@ void goto_convert_functionst::convert_function(
   f.body.update();
 
   if(hide(f.body))
-  {
     f.make_hidden();
-    symbol_table.get_writeable_ref(identifier).set_hidden();
-  }
 
   lifetime = parent_lifetime;
 }

src/goto-programs/goto_inline_class.cpp

@@ -256,7 +256,7 @@ void goto_inlinet::insert_function_body(
   end.type=LOCATION;
 
   // make sure the inlined function does not introduce hiding
-  if(ns.lookup(identifier).is_hidden())
+  if(goto_function.is_hidden())
   {
     for(auto &instruction : body.instructions)
       instruction.labels.remove(CPROVER_PREFIX "HIDE");

src/goto-programs/read_bin_goto_object.cpp

@@ -160,15 +160,7 @@ static bool read_bin_goto_object(
     f.body.update();
 
     if(hidden)
-    {
       f.make_hidden();
-      // can be removed with the next goto-binary version update as the
-      // information is guaranteed to be stored in the symbol table
-#if GOTO_BINARY_VERSION > 5
-#error This code should be removed
-#endif
-      symbol_table.get_writeable_ref(fname).set_hidden();
-    }
   }
 
   functions.compute_location_numbers();

src/goto-symex/symex_function_call.cpp

@@ -270,9 +270,8 @@ void goto_symext::symex_function_call_code(
       [&](const exprt &a) { return state.rename(a, ns); });
 
   // we hide the call if the caller and callee are both hidden
-  const bool callee_is_hidden = ns.lookup(identifier).is_hidden();
   const bool hidden =
-    state.call_stack().top().hidden_function && callee_is_hidden;
+    state.call_stack().top().hidden_function && goto_function.is_hidden();
 
   // record the call
   target.function_call(
@@ -338,7 +337,7 @@ void goto_symext::symex_function_call_code(
   frame.end_of_function=--goto_function.body.instructions.end();
   frame.return_value=call.lhs();
   frame.function_identifier=identifier;
-  frame.hidden_function = callee_is_hidden;
+  frame.hidden_function = goto_function.is_hidden();
 
   const framet &p_frame = state.call_stack().previous_frame();
   for(const auto &pair : p_frame.loop_iterations)

src/goto-symex/symex_main.cpp

@@ -434,8 +434,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
   state->call_stack().top().end_of_function = limit;
   state->call_stack().top().calling_location.pc =
     state->call_stack().top().end_of_function;
-  state->call_stack().top().hidden_function =
-    ns.lookup(entry_point_id).is_hidden();
+  state->call_stack().top().hidden_function = start_function->is_hidden();
 
   state->symex_target = &target;
 

src/util/symbol.h

@@ -117,19 +117,6 @@ class symbolt
     value = exprt(ID_compiled);
   }
 
-  /// Returns true iff the symbol is marked for internal use.
-  bool is_hidden() const
-  {
-    return is_auxiliary;
-  }
-
-  /// Mark a symbol for internal use. This is advisory and may be utilized,
-  /// e.g., to filter output.
-  void set_hidden()
-  {
-    is_auxiliary = true;
-  }
-
   /// Check that a symbol is well formed.
   bool is_well_formed() const;
 

unit/goto-instrument/cover/cover_only.cpp

@@ -22,7 +22,6 @@ symbolt create_new_symbol(const irep_idt &name, const irep_idt &file_name)
   source_locationt location;
   location.set_file(file_name);
   symbol.location = location;
-  symbol.type = code_typet{{}, empty_typet{}};
 
   return symbol;
 }