Skip to content
  • Xavier Leroy's avatar
    Add -main option to specify entrypoint function in interpreter mode (#374) · b1b853a2
    Xavier Leroy authored
    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.
    b1b853a2