goto-analyzer says __sputc is reachable in empty program

[markrtuttle]

CBMC version: 5.12 (cbmc-5.12-d8598f8-1270-g1ea1ede98)
Operating system: MacOS
Exact command line resulting in the issue: goto-analyzer --reachable-functions test.goto
What behaviour did you expect: Report main and __CPROVER_initialize reachable
What happened instead: Got also __sputc from stdio.h

I need help debugging odd behavior on MacOS. Consider the file test.c below.

#include <stdio.h>

int main(){
  return 0;
}

Run the commands

goto-cc -o test.goto test.c
goto-analyzer --reachable-functions test.goto

On MacOS, the result is unexpected:

/private/tmp/testing/test.c main 3 5
/Library/Developer/CommandLineTools/SDKs/MacOSX10.14.sdk/usr/include/stdio.h __sputc 264 269
/private/tmp/testing/<built-in-additions> __CPROVER_initialize 35 7

On Ubuntu 16, the result is expected:

/tmp/testing/test.c main 3 5
/tmp/testing/<built-in-additions> __CPROVER_initialize 35 7

[tautschnig]

This would require #2481 to be completed: __sputc is a function defined in stdio.h marked __attribute__((always_inline)), which we currently ignore.

[hannes-steffenhagen-diffblue]

Can still reproduce as of November 5th 2020

[martin-cs]

@hannes-steffenhagen-diffblue : does this mean you are working on this?

[feliperodri]

@hannes-steffenhagen-diffblue any updates on this issue? Should we close it?

[hannes-steffenhagen-diffblue]

I don't think this one should be closed, it just hasn't made it to the top of our backlog.

[martin-cs]

Might be effected by #5807

[markrtuttle]

The example still works as described with cbmc 5.37.