Simplified stdlib wrapper; use it only under MacOS X

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 21 insertions, 10 deletions

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 56bdb01..fcdc335 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -13,7 +13,7 @@
 open Printf
 open Clflags
 
-(* Location of the standard library *)
+(* Location of the compatibility library *)
 
 let stdlib_path = ref(
   try
@@ -47,9 +47,11 @@ let print_error oc msg =
 
 let preprocess ifile ofile =
   let cmd =
-    sprintf "%s -D__COMPCERT__ -I%s %s %s > %s"
+    sprintf "%s -D__COMPCERT__ %s %s %s > %s"
       Configuration.prepro
-      !stdlib_path
+      (if Configuration.need_stdlib_wrapper
+       then sprintf "-I%s" !stdlib_path
+       else "")
       (quote_options !prepro_options)
       ifile ofile in
   if command cmd <> 0 then begin
@@ -102,7 +104,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest PrintRTL.destination_cse option_dcse ".cse.rtl";
   set_dest PrintLTLin.destination option_dalloc ".alloc.ltl";
   (* Convert to Asm *)
-  let ppc =
+  let asm =
     match Compiler.transf_c_program csyntax with
     | Errors.OK x -> x
     | Errors.Error msg ->
@@ -110,7 +112,7 @@ let compile_c_file sourcename ifile ofile =
         exit 2 in
   (* Save asm *)
   let oc = open_out ofile in
-  PrintAsm.print_program oc ppc;
+  PrintAsm.print_program oc asm;
   close_out oc
 
 (* From Cminor to asm *)
@@ -161,11 +163,13 @@ let assemble ifile ofile =
 
 let linker exe_name files =
   let cmd =
-    sprintf "%s -o %s %s -L%s -lcompcert"
+    sprintf "%s -o %s %s %s"
       Configuration.linker
       (Filename.quote exe_name)
       (quote_options files)
-      !stdlib_path in
+      (if Configuration.need_stdlib_wrapper
+       then sprintf "-L%s -lcompcert" !stdlib_path
+       else "") in
   if command cmd <> 0 then exit 2
 
 (* Processing of a .c file *)
@@ -225,25 +229,32 @@ Preprocessing options:
   -U<symb>       Undefine preprocessor symbol
 Language support options (use -fno-<opt> to turn off -f<opt>) :
   -fbitfields    Emulate bit fields in structs [off]
-  -flonglong     Treat 'long long' as 'long' and 'long double' as 'double' [off]
+  -flonglong     Partial emulation of 'long long' types [on]
   -fstruct-passing  Emulate passing structs and unions by value [off]
   -fstruct-assign   Emulate assignment between structs or unions [off]
   -fvararg-calls Emulate calls to variable-argument functions [on]
 Code generation options:
-  -fmadd         Use fused multiply-add and multiply-sub instructions
+  -fmadd         Use fused multiply-add and multiply-sub instructions [off]
   -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
 Tracing options:
   -dparse        Save C file after parsing and elaboration in <file>.parse.c
   -dc            Save generated Compcert C in <file>.compcert.c
   -dclight       Save generated Clight in <file>.light.c
+  -dcminor       Save generated Cminor in <file>.cm
+  -drtl          Save unoptimized generated RTL in <file>.rtl
+  -dtailcall     Save RTL after tail call optimization in <file>.tailcall.rtl
+  -dcastopt      Save RTL after cast optimization in <file>.castopt.rtl
+  -dconstprop    Save RTL after constant propagation in <file>.constprop.rtl
+  -dcse          Save RTL after CSE optimization in <file>.cse.rtl
+  -dalloc        Save LTL after register allocation in <file>.alloc.ltl
   -dasm          Save generated assembly in <file>.s
 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)
 General options:
-  -stdlib <dir>  Set the path of the Compcert run-time library
+  -stdlib <dir>  Set the path of the Compcert run-time library [MacOS X only]
   -v             Print external commands before invoking them
 "