aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-08-16 10:35:17 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-08-16 10:35:17 +0200
commit5309f16159e4decd81330622dcdd6eb4b25819a1 (patch)
treeb40df6edcd7826e7d83885253508ccf49377479d
parenteb2844b87fa0e176bd65466d7ab7d16666344406 (diff)
downloadcompcert-kvx-5309f16159e4decd81330622dcdd6eb4b25819a1.tar.gz
compcert-kvx-5309f16159e4decd81330622dcdd6eb4b25819a1.zip
Moved quoting functions in Responsefile
Also corrected some typos and corrected exception handling for expandargv. Bug 18308
-rw-r--r--driver/Commandline.ml2
-rw-r--r--driver/Driveraux.ml36
-rw-r--r--driver/Linker.ml4
-rw-r--r--lib/Responsefile.mli11
-rw-r--r--lib/Responsefile.mll27
5 files changed, 44 insertions, 36 deletions
diff --git a/driver/Commandline.ml b/driver/Commandline.ml
index 7e683680..d125736a 100644
--- a/driver/Commandline.ml
+++ b/driver/Commandline.ml
@@ -103,6 +103,6 @@ let parse_cmdline spec =
try
let argv = expandargv Sys.argv in
parse_array spec argv 1 (Array.length argv - 1)
- with Arg.Bad s ->
+ with Responsefile.Error s ->
eprintf "%s" s;
exit 2
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index de1326ce..33cd9215 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -17,7 +17,7 @@ open Clflags
(* Is this a gnu based tool chain *)
let gnu_system = Configuration.system <> "diab"
-(* Sage removale of files *)
+(* Safe removal of files *)
let safe_remove file =
try Sys.remove file with Sys_error _ -> ()
@@ -58,46 +58,20 @@ let command stdout args =
argv.(0) fn (Unix.error_message err) param;
-1
-(* This function reimplements quoting of writeargv from libiberty *)
-let gnu_quote arg =
- let len = String.length arg in
- let buf = Buffer.create len in
- String.iter (fun c -> begin match c with
- | ' ' | '\t' | '\r' | '\n' | '\\' | '\'' | '"' ->
- Buffer.add_char buf '\\'
- | _ -> () end;
- Buffer.add_char buf c) arg;
- Buffer.contents buf
-
-let re_quote = Str.regexp ".*[ \t\n\r\"]"
-
-let diab_quote arg =
- let buf = Buffer.create ((String.length arg) + 8) in
- let doublequote = Str.string_match re_quote arg 0 in
- if doublequote then begin
- Buffer.add_char buf '"';
- String.iter (fun c ->
- if c = '"' then Buffer.add_char buf '\\';
- Buffer.add_char buf c) arg;
- if doublequote then Buffer.add_char buf '"';
- Buffer.contents buf
- end else
- arg
-
let command ?stdout args =
let resp = Sys.win32 && Configuration.response_file_style <> Configuration.Unsupported in
if resp && List.fold_left (fun len arg -> len + String.length arg + 1) 0 args > 7000 then
- let quote = match Configuration.response_file_style with
+ let quote,prefix = match Configuration.response_file_style with
| Configuration.Unsupported -> assert false
- | Configuration.Gnu -> gnu_quote
- | Configuration.Diab -> diab_quote in
+ | Configuration.Gnu -> Responsefile.gnu_quote,"@"
+ | Configuration.Diab -> Responsefile.diab_quote,"-@" in
let file,oc = Filename.open_temp_file "compcert" "" in
let cmd,args = match args with
| cmd::args -> cmd,args
| [] -> assert false (* Should never happen *) in
List.iter (fun a -> Printf.fprintf oc "%s " (quote a)) args;
close_out oc;
- let arg = if gnu_system then "@"^file else "-@"^file in
+ let arg = prefix^file in
let ret = command stdout [cmd;arg] in
safe_remove file;
ret
diff --git a/driver/Linker.ml b/driver/Linker.ml
index 305c5603..2f767023 100644
--- a/driver/Linker.ml
+++ b/driver/Linker.ml
@@ -24,8 +24,8 @@ let linker exe_name files =
["-o"; exe_name];
files;
(if Configuration.has_runtime_lib
- then ["-L" ^ !stdlib_path; "-lcompcert"]
- else [])
+ then ["-L" ^ !stdlib_path; "-lcompcert"]
+ else [])
] in
let exc = command cmd in
if exc <> 0 then begin
diff --git a/lib/Responsefile.mli b/lib/Responsefile.mli
index ec82c32e..ada5a15d 100644
--- a/lib/Responsefile.mli
+++ b/lib/Responsefile.mli
@@ -18,3 +18,14 @@
val expandargv: string array -> string array
(** Expand responsefile arguments contained in the array and return the full
set of arguments. *)
+
+exception Error of string
+ (** Raised by [expandargv] in case of an error *)
+
+val gnu_quote : string -> string
+ (** [gnu_quote arg] returns [arg] quoted compatible with the gnu tool chain
+ quoting conventions. *)
+
+val diab_quote : string -> string
+ (** [diab_quote arg] returns [arg] quoted compatible with the diab tool chain
+ quoting conventions. *)
diff --git a/lib/Responsefile.mll b/lib/Responsefile.mll
index bb29fd75..35a2dbdb 100644
--- a/lib/Responsefile.mll
+++ b/lib/Responsefile.mll
@@ -15,8 +15,6 @@
(* *********************************************************************)
-(* Parsing response files with various quoting styles *)
-
{
(* To accumulate the characters in a word or quoted string *)
let buf = Buffer.create 32
@@ -94,4 +92,29 @@ let expandargv argv =
let args = Array.to_list argv in
Array.of_list (List.rev (expand_args [] args []))
+(* This function reimplements quoting of writeargv from libiberty *)
+let gnu_quote arg =
+ let len = String.length arg in
+ let buf = Buffer.create len in
+ String.iter (fun c -> begin match c with
+ | ' ' | '\t' | '\r' | '\n' | '\\' | '\'' | '"' ->
+ Buffer.add_char buf '\\'
+ | _ -> () end;
+ Buffer.add_char buf c) arg;
+ Buffer.contents buf
+
+let re_quote = Str.regexp ".*[ \t\n\r\"]"
+
+let diab_quote arg =
+ let buf = Buffer.create ((String.length arg) + 8) in
+ let doublequote = Str.string_match re_quote arg 0 in
+ if doublequote then begin
+ Buffer.add_char buf '"';
+ String.iter (fun c ->
+ if c = '"' then Buffer.add_char buf '\\';
+ Buffer.add_char buf c) arg;
+ if doublequote then Buffer.add_char buf '"';
+ Buffer.contents buf
+ end else
+ arg
}