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.

1 files changed, 1 insertions, 1 deletions

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 ();