diff options
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 " |