From eba1a2fc06f269191407b734779b60b2e012b8e7 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 29 Feb 2012 10:01:18 +0000
Subject: Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt>

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1832 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Changelog         |  5 ++++-
 driver/Clflags.ml |  1 +
 driver/Driver.ml  | 18 ++++++++++++++++--
 3 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/Changelog b/Changelog
index 38553656..87220ca3 100644
--- a/Changelog
+++ b/Changelog
@@ -1,4 +1,4 @@
-Release 1.10, 2012-02-28
+Release 1.10, 2012-02-29
 ========================
 
 Improvements in confidence:
@@ -34,6 +34,9 @@ Performance improvements:
 Other improvements:
 - PowerPC/EABI: uninitialized global variables now go in common (bss) section.
 - PowerPC: work around limited excursion of conditional branch instructions.
+- Reference interpreter: better printing of pointer values and locations.
+- Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt> to pass
+  specific options to the preprocessor, assembler, or linker, respectively.
 
 
 Release 1.9.1, 2011-11-28
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 95f42092..2eb41477 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -14,6 +14,7 @@
 
 let prepro_options = ref ([]: string list)
 let linker_options = ref ([]: string list)
+let assembler_options = ref ([]: string list)
 let exe_name = ref "a.out"
 let option_flonglong = ref true
 let option_flongdouble = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 9813939b..443dbacb 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -169,8 +169,8 @@ let compile_cminor_file ifile ofile =
 
 let assemble ifile ofile =
   let cmd =
-    sprintf "%s -o %s %s"
-      Configuration.asm ofile ifile in
+    sprintf "%s -o %s %s %s"
+      Configuration.asm ofile (quote_options !assembler_options) ifile in
   let retcode = command cmd in
   if retcode <> 0 then begin
     safe_remove ofile;
@@ -257,6 +257,11 @@ let process_S_file sourcename =
 
 (* Command-line parsing *)
 
+let explode_comma_option s =
+  match Str.split (Str.regexp ",") s with
+  | [] -> assert false
+  | hd :: tl -> tl
+
 type action =
   | Set of bool ref
   | Unset of bool ref
@@ -327,6 +332,7 @@ Preprocessing options:
   -I<dir>        Add <dir> to search path for #include files
   -D<symb>=<val> Define preprocessor symbol
   -U<symb>       Undefine preprocessor symbol
+  -Wp,<opt>      Pass option <opt> to the preprocessor
 Language support options (use -fno-<opt> to turn off -f<opt>) :
   -fbitfields    Emulate bit fields in structs [off]
   -flonglong     Partial emulation of 'long long' types [on]
@@ -341,6 +347,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) :
   -fsse          (IA32) Use SSE2 instructions for some integer operations [on]
   -fsmall-data <n>  Set maximal size <n> for allocation in small data area
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
+  -Wa,<opt>      Pass option <opt> to the assembler
 Tracing options:
   -dparse        Save C file after parsing and elaboration in <file>.parse.c
   -dc            Save generated Compcert C in <file>.compcert.c
@@ -358,6 +365,7 @@ Linking options:
   -l<lib>        Link library <lib>
   -L<dir>        Add <dir> to search path for libraries
   -o <file>      Generate executable in <file> (default: a.out)
+  -Wl,<opt>      Pass option <opt> to the linker
 General options:
   -stdlib <dir>  Set the path of the Compcert run-time library [MacOS X only]
   -v             Print external commands before invoking them
@@ -420,6 +428,12 @@ let cmdline_actions =
       linker_options := objfile :: !linker_options);
   ".*\\.[oa]$", Self (fun s ->
       linker_options := s :: !linker_options);
+  "-Wp,", Self (fun s ->
+      prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
+  "-Wa,", Self (fun s ->
+      assembler_options := s :: !assembler_options);
+  "-Wl,", Self (fun s ->
+      linker_options := s :: !linker_options);
   "-fsmall-data$", Integer(fun n -> option_small_data := n);
   "-fsmall-const$", Integer(fun n -> option_small_const := n);
   "-fall$", Self (fun _ ->
-- 
cgit