diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-04 09:29:08 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-04 09:29:08 +0000 |
commit | ba9cd4f93ef991fa3794d333e8da19878df06e2d (patch) | |
tree | d0870ebda361f8f07f930053403d832473824e6b /driver/Driver.ml | |
parent | 601569c2e0c9ec4748eefcbdb9f62c93f8aa822c (diff) | |
download | compcert-ba9cd4f93ef991fa3794d333e8da19878df06e2d.tar.gz compcert-ba9cd4f93ef991fa3794d333e8da19878df06e2d.zip |
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
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r-- | driver/Driver.ml | 31 |
1 files changed, 21 insertions, 10 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 56bdb01c..fcdc3355 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 " |