Error 'The program has no entry point' on goto-binary without main(), although --function is given

[peterschrammel]

when --function is given, cbmc should analyze the binary regardless of the presence of a main() function

[tautschnig]

Isn't it even worse in that --function no longer works at all?

[tautschnig]

Apologies, here is what works:

• cbmc --function foo foo.c
• goto-cc --function foo foo.o -o foo ; cbmc foo

Maybe there should just be helpful output stating that --function cannot be used with goto binaries, and goto-cc should be used instead.

[peterschrammel]

Yes, that works. But it's totally impracticable to recompile the goto-binaries for each function...

[peterschrammel]

@tautschnig, is there any fundamental reason why --function does not work with goto-binaries?

[tautschnig]

The problem is that the entry point (_start) would have to be thrown away and rebuilt. It shouldn't be a big deal to do that (actually I had been doing this in fshell because it permitted re-setting the entry point at runtime), just a bit of care. The code can't be re-used as-is, but here's what I had been doing: https://github.com/tautschnig/fshell/blob/master/fshell2/command/command_processing.cpp#L596