aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-02-13 15:39:07 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-02-13 15:39:07 +0100
commit5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb (patch)
tree13266f8767648ee5433f30b16ec503144c67d003 /driver
parent236d8a48288ea5845466408cf9d0be2ccd68f9a8 (diff)
downloadcompcert-kvx-5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb.tar.gz
compcert-kvx-5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb.zip
Introduced configuration variable for gnu systems.
The variable gnu_toolchain is true if a gnu toolchain is used and false in all other cases. The variable avoids the explicit test whether the system string is diab and should be easier to change. Bug 20521.
Diffstat (limited to 'driver')
-rw-r--r--driver/Assembler.ml4
-rw-r--r--driver/Configuration.ml26
-rw-r--r--driver/Configuration.mli3
-rw-r--r--driver/Driveraux.ml3
-rw-r--r--driver/Driveraux.mli3
-rw-r--r--driver/Frontend.ml4
-rw-r--r--driver/Linker.ml6
7 files changed, 21 insertions, 28 deletions
diff --git a/driver/Assembler.ml b/driver/Assembler.ml
index 1d91ef50..ba9351ca 100644
--- a/driver/Assembler.ml
+++ b/driver/Assembler.ml
@@ -32,11 +32,11 @@ let assemble ifile ofile =
end
let assembler_actions =
- [ Prefix "-Wa,", Self (fun s -> if gnu_system then
+ [ Prefix "-Wa,", Self (fun s -> if Configuration.gnu_toolchain then
assembler_options := s :: !assembler_options
else
assembler_options := List.rev_append (explode_comma_option s) !assembler_options);
- Exact "-Xassembler", String (fun s -> if gnu_system then
+ Exact "-Xassembler", String (fun s -> if Configuration.gnu_toolchain then
assembler_options := s::"-Xassembler":: !assembler_options
else
assembler_options := s::!assembler_options );]
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 5d5b4a2d..87e72f1c 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -115,6 +115,12 @@ let asm =
let linker =
tool_absolute_path (get_config_list "linker")@(opt_config_list "linker_options")
+let get_bool_config key =
+ match get_config_string key with
+ | "true" -> true
+ | "false" -> false
+ | v -> bad_config key [v]
+
let arch =
match get_config_string "arch" with
| "powerpc"|"arm"|"x86" as a -> a
@@ -127,27 +133,15 @@ let is_big_endian =
| "little" -> false
| v -> bad_config "endianness" [v]
let system = get_config_string "system"
-let has_runtime_lib =
- match get_config_string "has_runtime_lib" with
- | "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 has_runtime_lib = get_bool_config "has_runtime_lib"
+let has_standard_headers = get_bool_config "has_standard_headers"
let stdlib_path =
if has_runtime_lib then
let path = get_config_string "stdlib_path" in
absolute_path ini_dir path
else
""
-let asm_supports_cfi =
- match get_config_string "asm_supports_cfi" with
- | "true" -> true
- | "false" -> false
- | v -> bad_config "asm_supports_cfi" [v]
+let asm_supports_cfi = get_bool_config "asm_supports_cfi"
type struct_passing_style =
@@ -188,3 +182,5 @@ let response_file_style =
| "gnu" -> Gnu
| "diab" -> Diab
| v -> bad_config "response_file_style" [v]
+
+let gnu_toolchain = system <> "diab"
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index 197e8ad2..f0bb8f83 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -74,3 +74,6 @@ type response_file_style =
val response_file_style: response_file_style
(** Style of supported responsefiles *)
+
+val gnu_toolchain: bool
+ (** Does the targeted system use the gnu toolchain *)
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index d25301d2..2c478fb1 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -14,9 +14,6 @@
open Printf
open Clflags
-(* Is this a gnu based tool chain *)
-let gnu_system = Configuration.system <> "diab"
-
(* Safe removal of files *)
let safe_remove file =
try Sys.remove file with Sys_error _ -> ()
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli
index e6bac6e3..274ecedd 100644
--- a/driver/Driveraux.mli
+++ b/driver/Driveraux.mli
@@ -36,9 +36,6 @@ val ensure_inputfile_exists: string -> unit
val print_error:out_channel -> Errors.errcode list -> unit
(** Printing of error messages *)
-val gnu_system: bool
- (** Are the target tools gnu tools? *)
-
val explode_comma_option: string -> string list
(** Split option at commas *)
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 41ca3bb8..b4b161b0 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -125,7 +125,7 @@ let prepro_actions = [
Exact "-Xpreprocessor", String (fun s ->
prepro_options := s :: !prepro_options);
Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options);]
- @ (if gnu_system then gnu_prepro_actions else [])
+ @ (if Configuration.gnu_toolchain then gnu_prepro_actions else [])
let gnu_prepro_help =
{| -M Ouput a rule suitable for make describing the
@@ -163,4 +163,4 @@ let prepro_help = {|Preprocessing options:
-Wp,<opt> Pass option <opt> to the preprocessor
-Xpreprocessor <opt> Pass option <opt> to the preprocessor
|}
- ^ (if gnu_system then gnu_prepro_help else "")
+ ^ (if Configuration.gnu_toolchain then gnu_prepro_help else "")
diff --git a/driver/Linker.ml b/driver/Linker.ml
index 5e14cfd4..54566efb 100644
--- a/driver/Linker.ml
+++ b/driver/Linker.ml
@@ -48,7 +48,7 @@ let linker_help =
-l<lib> Link library <lib>
-L<dir> Add <dir> to search path for libraries
|} ^
- (if gnu_system then gnu_linker_help else "") ^
+ (if Configuration.gnu_toolchain then gnu_linker_help else "") ^
{| -s Remove all symbol table and relocation information from the
executable
-static Prevent linking with the shared libraries
@@ -63,14 +63,14 @@ let linker_help =
let linker_actions =
[ Prefix "-l", Self push_linker_arg;
Prefix "-L", Self push_linker_arg; ] @
- (if gnu_system then
+ (if Configuration.gnu_toolchain then
[ Exact "-nostartfiles", Self push_linker_arg;
Exact "-nodefaultlibs", Self push_linker_arg;
Exact "-nostdlib", Self push_linker_arg;]
else []) @
[ Exact "-s", Self push_linker_arg;
Exact "-static", Self push_linker_arg;
- Exact "-T", String (fun s -> if gnu_system then begin
+ Exact "-T", String (fun s -> if Configuration.gnu_toolchain then begin
push_linker_arg ("-T");
push_linker_arg(s)
end else