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