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/Clflags.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/Clflags.ml')
| -rw-r--r-- | driver/Clflags.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2db9399f..80883372 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -67,3 +67,4 @@ let option_small_const = ref (!option_small_data) let option_timings = ref false let stdlib_path = ref Configuration.stdlib_path let use_standard_headers = ref Configuration.has_standard_headers +let main_function_name = ref "main" |