From 0c84a608141523ac6f4c12cb8183eff3bfa42039 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 30 Nov 2015 17:06:04 +0100 Subject: Allow relative library path. The path to the libcompert folder can be specified relative to the location of the compcert.ini file. Bug 17431 --- driver/Configuration.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 50e251c4..b9153c36 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -21,12 +21,18 @@ let search_argv key = done; !res +let absolute_path base file = + if Filename.is_relative file then + Filename.concat base file + else + file + (* Locate the .ini file, which is either in the same directory as the executable or in the directory ../share *) let ini_file_name = match search_argv "--conf" with - | Some s -> s + | Some s -> absolute_path (Sys.getcwd ()) s | None -> try Sys.getenv "COMPCERT_CONFIG" @@ -47,6 +53,8 @@ let ini_file_name = exit 2 end +let ini_dir = Filename.dirname ini_file_name + (* Read in the .ini file *) let _ = @@ -104,7 +112,8 @@ let has_standard_headers = | v -> bad_config "has_standard_headers" [v] let stdlib_path = if has_runtime_lib then - get_config_string "stdlib_path" + let path = get_config_string "stdlib_path" in + absolute_path ini_dir path else "" let asm_supports_cfi = -- cgit From 7b0ce5abd6a31a3790dfcfd3be69064bd5ca5eb3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 1 Dec 2015 15:27:16 +0100 Subject: Allow relative paths for the tools. The tools now can be specified by 3 ways: -Relative to the compcert.ini file -With absolute path to the location -As a simple filename which lies on the PATH variable. Bug 17431 --- driver/Configuration.ml | 31 +++++++++++++++++++++---------- 1 file changed, 21 insertions(+), 10 deletions(-) diff --git a/driver/Configuration.ml b/driver/Configuration.ml index b9153c36..8ab2642c 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +open Filename open Printf let search_argv key = @@ -22,8 +23,8 @@ let search_argv key = !res let absolute_path base file = - if Filename.is_relative file then - Filename.concat base file + if is_relative file then + concat base file else file @@ -37,14 +38,14 @@ let ini_file_name = try Sys.getenv "COMPCERT_CONFIG" with Not_found -> - let exe_dir = Filename.dirname Sys.executable_name in + let exe_dir = dirname Sys.executable_name in let share_dir = - Filename.concat (Filename.concat exe_dir Filename.parent_dir_name) + concat (concat exe_dir parent_dir_name) "share" in let share_compcert_dir = - Filename.concat share_dir "compcert" in + concat share_dir "compcert" in let search_path = [exe_dir;share_dir;share_compcert_dir] in - let files = List.map (fun s -> Filename.concat s "compcert.ini") search_path in + let files = List.map (fun s -> concat s "compcert.ini") search_path in try List.find Sys.file_exists files with Not_found -> @@ -53,7 +54,7 @@ let ini_file_name = exit 2 end -let ini_dir = Filename.dirname ini_file_name +let ini_dir = dirname ini_file_name (* Read in the .ini file *) @@ -90,9 +91,19 @@ let get_config_list key = | [] -> bad_config key [] | vl -> vl -let prepro = get_config_list "prepro" -let asm = get_config_list "asm" -let linker = get_config_list "linker" +let tool_absolute_path tools = + match tools with + | [] -> [] + | tool::args -> let tool = + if is_implicit tool && dirname tool = current_dir_name then + tool + else + absolute_path ini_dir tool in + tool::args + +let prepro = tool_absolute_path (get_config_list "prepro") +let asm = tool_absolute_path (get_config_list "asm") +let linker = tool_absolute_path (get_config_list "linker") let arch = match get_config_string "arch" with | "powerpc"|"arm"|"ia32" as a -> a -- cgit From e1b0d579d7c0971856a3ada74078e51b3797a30a Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 11 Dec 2015 13:30:26 +0100 Subject: Add a target option. This option allows it to specify a .ini file that is in the usual search path. Bug 17431 --- driver/Configuration.ml | 7 +++++-- driver/Driver.ml | 3 ++- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 8ab2642c..91d9a397 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -32,12 +32,15 @@ let absolute_path base file = the executable or in the directory ../share *) let ini_file_name = - match search_argv "--conf" with + match search_argv "-conf" with | Some s -> absolute_path (Sys.getcwd ()) s | None -> try Sys.getenv "COMPCERT_CONFIG" with Not_found -> + let ini_name = match search_argv "-target" with + | Some s -> s^".ini" + | None -> "compcert.ini" in let exe_dir = dirname Sys.executable_name in let share_dir = concat (concat exe_dir parent_dir_name) @@ -45,7 +48,7 @@ let ini_file_name = let share_compcert_dir = concat share_dir "compcert" in let search_path = [exe_dir;share_dir;share_compcert_dir] in - let files = List.map (fun s -> concat s "compcert.ini") search_path in + let files = List.map (fun s -> concat s ini_name) search_path in try List.find Sys.file_exists files with Not_found -> diff --git a/driver/Driver.ml b/driver/Driver.ml index 8d144ad5..c9c16eac 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -572,7 +572,8 @@ let cmdline_actions = Exact "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n); Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); (* Target processor options *) - Exact "--conf", String (fun _ -> ()); (* Ignore option since it is already handled *) + Exact "-conf", String (fun _ -> ()); (* Ignore option since it is already handled *) + Exact "-target", String (fun _ -> ()); (* Ignore option since it is already handled *) Exact "-mthumb", Set option_mthumb; Exact "-marm", Unset option_mthumb; (* Assembling options *) -- cgit From 36fa22560e2a289c9f75f0fe058b72eaad6d53b4 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 11 Dec 2015 21:02:56 +0100 Subject: Removed the open Filename. --- driver/Configuration.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 91d9a397..3025391b 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -10,7 +10,6 @@ (* *) (* *********************************************************************) -open Filename open Printf let search_argv key = @@ -23,8 +22,8 @@ let search_argv key = !res let absolute_path base file = - if is_relative file then - concat base file + if Filename.is_relative file then + Filename.concat base file else file @@ -41,14 +40,14 @@ let ini_file_name = let ini_name = match search_argv "-target" with | Some s -> s^".ini" | None -> "compcert.ini" in - let exe_dir = dirname Sys.executable_name in + let exe_dir = Filename.dirname Sys.executable_name in let share_dir = - concat (concat exe_dir parent_dir_name) + Filename.concat (Filename.concat exe_dir Filename.parent_dir_name) "share" in let share_compcert_dir = - concat share_dir "compcert" in + Filename.concat share_dir "compcert" in let search_path = [exe_dir;share_dir;share_compcert_dir] in - let files = List.map (fun s -> concat s ini_name) search_path in + let files = List.map (fun s -> Filename.concat s ini_name) search_path in try List.find Sys.file_exists files with Not_found -> @@ -57,7 +56,7 @@ let ini_file_name = exit 2 end -let ini_dir = dirname ini_file_name +let ini_dir = Filename.dirname ini_file_name (* Read in the .ini file *) @@ -98,7 +97,7 @@ let tool_absolute_path tools = match tools with | [] -> [] | tool::args -> let tool = - if is_implicit tool && dirname tool = current_dir_name then + if Filename.is_implicit tool && Filename.dirname tool = Filename.current_dir_name then tool else absolute_path ini_dir tool in -- cgit