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

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

from cbmc.

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.

from cbmc.

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

from cbmc.

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

from cbmc.

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

from cbmc.