diff options
| author | Michael Schmidt <github@mschmidt.me> | 2016-12-16 12:37:55 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2016-12-16 12:37:55 +0100 |
| commit | e65eeecf7f34076cbfad6876ec21623ad25e9cf7 (patch) | |
| tree | b72bb3e5e0b3b83c6df7fa451a8188790d6ad6b3 /driver | |
| parent | a48f857450950b2d1370249bca673ad2c15559d1 (diff) | |
| download | compcert-e65eeecf7f34076cbfad6876ec21623ad25e9cf7.tar.gz compcert-e65eeecf7f34076cbfad6876ec21623ad25e9cf7.zip | |
add parameter to enforce a specific compcert build number for QSKs (bug 20595)
Diffstat (limited to 'driver')
| -rwxr-xr-x[-rw-r--r--] | driver/Driver.ml | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 353a7176..e3b9ec52 100644..100755 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -348,6 +348,13 @@ let print_usage_and_exit () = let print_version_and_exit () = printf "%s" version_string; exit 0 +let enforce_buildnr nr = + let build = int_of_string Version.buildnr in + if nr != build then begin + eprintf "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\ +Please use matching builds of QSK and CompCert.\n" build nr; exit 2 + end + let language_support_options = [ option_fbitfields; option_flongdouble; option_fstruct_passing; option_fvararg_calls; option_funprototyped; @@ -374,9 +381,14 @@ let cmdline_actions = Exact "--help", Unit print_usage_and_exit; (* Getting version info *) Exact "-version", Unit print_version_and_exit; - Exact "--version", Unit print_version_and_exit; + Exact "--version", Unit print_version_and_exit;] @ +(* Enforcing CompCert build numbers for QSKs *) + (if Version.buildnr <> "" then + [ Exact "-qsk-enforce-build", Integer enforce_buildnr; + Exact "--qsk-enforce-build", Integer enforce_buildnr; ] + else []) @ (* Processing options *) - Exact "-c", Set option_c; + [ Exact "-c", Set option_c; Exact "-E", Set option_E; Exact "-S", Set option_S; Exact "-o", String(fun s -> option_o := Some s); |