diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-10-30 18:32:04 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-30 18:32:04 +0100 |
| commit | b1b853a2e9f7f2143fedd58772a702bc9c6a8ba1 (patch) | |
| tree | 6291dad029ddd029db371a4d6bc4101d15db6cb9 /driver/Driver.ml | |
| parent | 6aeb6455cc52172fbb78999b17503d9a66ce7bfb (diff) | |
| download | compcert-kvx-b1b853a2e9f7f2143fedd58772a702bc9c6a8ba1.tar.gz compcert-kvx-b1b853a2e9f7f2143fedd58772a702bc9c6a8ba1.zip | |
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.
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 66cfeaa7..043e43c1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -233,6 +233,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -trace Have the interpreter produce a detailed trace of reductions -random Randomize execution order -all Simulate all possible execution orders + -main <name> Start executing at function <name> instead of main() |} let print_usage_and_exit () = @@ -355,7 +356,8 @@ let cmdline_actions = Exact "-quiet", Unit (fun () -> Interp.trace := 0); Exact "-trace", Unit (fun () -> Interp.trace := 2); Exact "-random", Unit (fun () -> Interp.mode := Interp.Random); - Exact "-all", Unit (fun () -> Interp.mode := Interp.All) + Exact "-all", Unit (fun () -> Interp.mode := Interp.All); + Exact "-main", String (fun s -> main_function_name := s) ] (* Optimization options *) (* -f options: come in -f and -fno- variants *) |