Add -main option to specify entrypoint function in interpreter mode

[xavierleroy]

As suggested by a user. When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function.

This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option.

The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.

[tankf33der]

I've got what I needed and tested successfully - monocypher library passed via new command line interface.

@LoupVaillant
I will use this feature for automatically testing for next releases.

[xavierleroy]

Thanks a lot @tankf33der for the fast testing!

I have a good feeling about this new feature, so I'll merge right now.

[m-schmidt]

I think one should extend the patch. Elab.ml contains some checks for main which still use the hardcoded string literal "main". E.g. the one for misdeclaration as inline, _Noreturn, etc.

[m-schmidt]

Also, I suggest to disallow the new option in compiler mode or let it take effect only in interpreter mode.

[xavierleroy]

I think one should extend the patch. Elab.ml contains some checks for main which still use the hardcoded string literal "main". E.g. the one for misdeclaration as inline, _Noreturn, etc.

For the purpose of testing with the interpreter, it's fine if the alternate entry point is inline, _Noreturn, etc. So I'm not sure any of the standard restrictions on main() should be applied to the alternate entry point.

Also, I suggest to disallow the new option in compiler mode or let it take effect only in interpreter mode.

This I agree with.

[xavierleroy]

Commit b40aef6 makes sure that -main is used only in conjunction with -interp.