From b1b853a2e9f7f2143fedd58772a702bc9c6a8ba1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 30 Oct 2020 18:32:04 +0100 Subject: Add -main option to specify entrypoint function in interpreter mode (#374) 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. --- cfrontend/C2C.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 2386eed9..ef028255 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1495,7 +1495,7 @@ let convertProgram p = let p' = { prog_defs = gl2; prog_public = public_globals gl2; - prog_main = intern_string "main"; + prog_main = intern_string !Clflags.main_function_name; prog_types = typs; prog_comp_env = ce } in Diagnostics.check_errors (); -- cgit