From ae7eeb880d35fb12b4620e5320a8f9677a72d159 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 2 Jul 2020 15:30:58 +0200 Subject: Remove no longer needed option enforce-buildnr --- driver/Driver.ml | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index be1252f9..66cfeaa7 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -238,12 +238,6 @@ Code generation options: (use -fno- to turn off -f) let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let enforce_buildnr nr = - let build = int_of_string Version.buildnr in - if nr != build then - fatal_error no_loc "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\ -Please use matching builds of QSK and CompCert." build nr - let dump_mnemonics destfile = let oc = open_out_bin destfile in let pp = Format.formatter_of_out_channel oc in @@ -279,10 +273,7 @@ let cmdline_actions = @ version_options tool_name @ (* Enforcing CompCert build numbers for QSKs and mnemonics dump *) (if Version.buildnr <> "" then - [ Exact "-qsk-enforce-build", Integer enforce_buildnr; - Exact "--qsk-enforce-build", Integer enforce_buildnr; - Exact "-dump-mnemonics", String dump_mnemonics; - ] + [Exact "-dump-mnemonics", String dump_mnemonics;] else []) @ (* Processing options *) [ Exact "-c", Set option_c; -- cgit 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. --- driver/Driver.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'driver/Driver.ml') 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- to turn off -f) -trace Have the interpreter produce a detailed trace of reductions -random Randomize execution order -all Simulate all possible execution orders + -main Start executing at function 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 *) -- cgit