diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-instrument/cover_filter.cpp
index 03f6b1e2f9e..60c6ecf8d1a 100644
--- a/src/goto-instrument/cover_filter.cpp
+++ b/src/goto-instrument/cover_filter.cpp
@@ -29,7 +29,7 @@ bool internal_functions_filtert::operator()(
   if(function.name == INITIALIZE_FUNCTION)
     return false;
 
-  if(goto_function.is_hidden())
+  if(function.is_hidden())
     return false;
 
   // ignore Java built-ins (synthetic functions)
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 3512b84a3fa..24f515685e5 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -215,7 +215,10 @@ 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;
 }
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
index 96dbd04eef4..fdb8fd9c287 100644
--- a/src/goto-programs/goto_inline_class.cpp
+++ b/src/goto-programs/goto_inline_class.cpp
@@ -253,7 +253,7 @@ void goto_inlinet::insert_function_body(
   end.type=LOCATION;
 
   // make sure the inlined function does not introduce hiding
-  if(goto_function.is_hidden())
+  if(ns.lookup(identifier).is_hidden())
   {
     for(auto &instruction : body.instructions)
       instruction.labels.remove(CPROVER_PREFIX "HIDE");
diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp
index 775d0f4c545..09fbebd9a53 100644
--- a/src/goto-programs/read_bin_goto_object.cpp
+++ b/src/goto-programs/read_bin_goto_object.cpp
@@ -160,7 +160,15 @@ 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();
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index add84eae5ba..36a27757a40 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -274,8 +274,9 @@ void goto_symext::symex_function_call_code(
     a = state.rename(std::move(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 && goto_function.is_hidden();
+    state.call_stack().top().hidden_function && callee_is_hidden;
 
   // record the call
   target.function_call(
@@ -314,7 +315,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=goto_function.is_hidden();
+  frame.hidden_function = callee_is_hidden;
 
   const framet &p_frame = state.call_stack().previous_frame();
   for(const auto &pair : p_frame.loop_iterations)
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 82233ed2406..7f34603829f 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -326,7 +326,8 @@ 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 = start_function->is_hidden();
+  state->call_stack().top().hidden_function =
+    ns.lookup(entry_point_id).is_hidden();
 
   state->symex_target = &target;
 
diff --git a/src/util/symbol.h b/src/util/symbol.h
index d34c8351c43..d83e7581418 100644
--- a/src/util/symbol.h
+++ b/src/util/symbol.h
@@ -117,6 +117,19 @@ 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;
 
diff --git a/unit/goto-instrument/cover/cover_only.cpp b/unit/goto-instrument/cover/cover_only.cpp
index 68c413f7253..c6083206108 100644
--- a/unit/goto-instrument/cover/cover_only.cpp
+++ b/unit/goto-instrument/cover/cover_only.cpp
@@ -22,6 +22,7 @@ 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;
 }