`goto-cc --export-file-local-symbols` does not export symbols that are only used in contracts.

[remi-delmas-3000]

CBMC version: 5.71.0
Operating system:all
Exact command line resulting in the issue: goto-cc --export-file-local-symbols main.c
What behaviour did you expect: The static local symbol vtable_0 is present in the symbol table in mangled form
What happened instead: The static local symbol vtable_0 is absent from the symbol table.

It seems like the pass that checks if a file-local symbol needs to be exported does not search in contract clauses.

#include <stdbool.h>
#include <stdlib.h>

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(NULL == vtable || &vtable_0 == vtable)
{
  if(vtable->f)
    vtable->f();
}

int main()
{
  vtable_t *vtable;
  foo(vtable);
}

goto-cc --export-file-local-symbols main.c
goto-instrument --show-symbol-table | grep vtable_0
// grep result empty

[tautschnig]

There indeed is a bug, but I should note that name-mangling objects via this route is not supported: #6356 was closed in favour of using crangler (which would have worked around the actual problem here). I'll issue a PR fixing the bug (which is that we spuriously remove the vtable_0 object, which is wrong even when not exporting file-local objects).