Remove internal symbols: keep all symbols used in contracts

In beb1353 we had chosen to only keep code-typed symbols, but indeed
we also need to retain objects (only) referred to from contracts.

Also add debug-level status information of what symbols are being
removed (which is information I have previously needed more than once in
debugging, and it's also now the only actual use of the messaget that we
already had in place).

Fixes: #7414

Author: tautschnig

regression/ansi-c/static5/main.c

@@ -0,0 +1,24 @@
+typedef struct vtable_s
+{
+  int (*f)(void);
+} vtable_t;
+
+int return_0()
+{
+  return 0;
+}
+
+static vtable_t vtable_0 = {.f = &return_0};
+
+void foo(vtable_t *vtable)
+  __CPROVER_requires((void *)0 == vtable || &vtable_0 == vtable)
+{
+  if(vtable->f)
+    vtable->f();
+}
+
+int main()
+{
+  vtable_t *vtable;
+  foo(vtable);
+}

regression/ansi-c/static5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--verbosity 10
+^Removing unused symbol
+^EXIT=0$
+^SIGNAL=0$
+--
+^Removing unused symbol vtable_0$

src/linking/remove_internal_symbols.cpp

@@ -76,16 +76,8 @@ static void get_symbols(
 
       for(const auto &s : new_symbols)
       {
-        // keep functions called in contracts within scope.
-        // should we keep local variables from the contract as well?
-        const symbolt *new_symbol = nullptr;
-        if(!ns.lookup(s, new_symbol))
-        {
-          if(new_symbol->type.id() == ID_code)
-          {
-            working_set.push_back(new_symbol);
-          }
-        }
+        if(s != CPROVER_PREFIX "return_value")
+          working_set.push_back(&ns.lookup(s));
       }
     }
   }
@@ -239,6 +231,7 @@ void remove_internal_symbols(
     if(exported.find(it->first)==exported.end())
     {
       symbol_table_baset::symbolst::const_iterator next = std::next(it);
+      log.debug() << "Removing unused symbol " << it->first << messaget::eom;
       symbol_table.erase(it);
       it=next;
     }