#include <stdio.h>
int some_symbol (void);
int main (int argc, char *argv[]) {
int ret = some_symbol ();
if (ret == 1)
return 0;
fprintf (stderr, "ret was %i instead of 1\n", ret);
return -1;
}