Merge pull request #7417 from tautschnig/bugfixes/7414-contract-static

Remove internal symbols: keep all symbols used in contracts

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,11 @@ 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);
-          }
-        }
+        const symbolt *symbol_ptr;
+        // identifiers for parameters of prototypes need not exist, and neither
+        // does __CPROVER_return_value
+        if(!ns.lookup(s, symbol_ptr))
+          working_set.push_back(symbol_ptr);
       }
     }
   }
@@ -239,6 +234,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;
     }