diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-06-17 18:53:39 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-06-17 18:53:39 +0200 |
| commit | b51cc596555dae929e75e4a02520f01d6f53978d (patch) | |
| tree | 7a43ce306cb641b85dab43e88ed757edb873eed2 /driver | |
| parent | e503983cdc99c6038ada0d0b94f32f02d13210c8 (diff) | |
| parent | 0e9ededa8c1d194453f5113bf57c93d0803f03b1 (diff) | |
| download | compcert-kvx-b51cc596555dae929e75e4a02520f01d6f53978d.tar.gz compcert-kvx-b51cc596555dae929e75e4a02520f01d6f53978d.zip | |
Merge branch 'master' into json_export
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Configuration.ml | 5 | ||||
| -rw-r--r-- | driver/Configuration.mli | 2 | ||||
| -rw-r--r-- | driver/Driver.ml | 6 | ||||
| -rw-r--r-- | driver/Interp.ml | 2 |
4 files changed, 12 insertions, 3 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 2cea2b80..70131fc6 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -82,6 +82,11 @@ let has_runtime_lib = | "true" -> true | "false" -> false | v -> bad_config "has_runtime_lib" [v] +let has_standard_headers = + match get_config_string "has_standard_headers" with + | "true" -> true + | "false" -> false + | v -> bad_config "has_standard_headers" [v] let stdlib_path = if has_runtime_lib then get_config_string "stdlib_path" diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 20c45518..72810456 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -31,6 +31,8 @@ val stdlib_path: string (** Path to CompCert's library *) val has_runtime_lib: bool (** True if CompCert's library is available. *) +val has_standard_headers: bool + (** True if CompCert's standard header files is available. *) val advanced_debug: bool (** True if advanced debug is implement for the Target *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 90badb85..352483bf 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -93,8 +93,8 @@ let preprocess ifile ofile = let cmd = List.concat [ Configuration.prepro; ["-D__COMPCERT__"]; - (if Configuration.has_runtime_lib - then ["-I" ^ !stdlib_path] + (if Configuration.has_standard_headers + then ["-I" ^ Filename.concat !stdlib_path "include" ] else []); List.rev !prepro_options; [ifile] @@ -515,6 +515,8 @@ let cmdline_actions = Exact "-E", Set option_E; Exact "-S", Set option_S; Exact "-o", String(fun s -> option_o := Some s); + Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in + option_o := Some s); (* Preprocessing options *) Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options); diff --git a/driver/Interp.ml b/driver/Interp.ml index b16d2cae..f453af95 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -402,7 +402,7 @@ let do_inline_assembly txt sg ge w args m = None (* Implementing external functions producing observable events *) let rec world ge m = - Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m) + lazy (Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m)) and world_io ge m id args = None |