diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
commit | 255cee09b71255051c2b40eae0c88bffce1f6f32 (patch) | |
tree | 7951b1b13e8fd5e525b9223e8be0580e83550f55 /driver/Driver.ml | |
parent | 6e5041958df01c56762e90770abd704b95a36e5d (diff) |
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
1- new register allocator (+ live range splitting, spilling&reloading, etc)
based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r-- | driver/Driver.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 3a5981e..eb0e004 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -89,6 +89,7 @@ let parse_c_file sourcename ifile = (* Simplification options *) let simplifs = "b" (* blocks: mandatory *) +(* ^ (if !option_flonglong then "l" else "") *) ^ (if !option_fstruct_return then "s" else "") ^ (if !option_fbitfields then "f" else "") ^ (if !option_fpacked_structs then "p" else "") @@ -148,7 +149,8 @@ let compile_c_ast sourcename csyntax ofile = set_dest PrintRTL.destination_inlining option_dinlining ".inlining.rtl"; set_dest PrintRTL.destination_constprop option_dconstprop ".constprop.rtl"; set_dest PrintRTL.destination_cse option_dcse ".cse.rtl"; - set_dest PrintLTLin.destination option_dalloc ".alloc.ltl"; + set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; + set_dest PrintLTL.destination option_dalloc ".alloc.ltl"; set_dest PrintMach.destination option_dmach ".mach"; (* Convert to Asm *) let asm = @@ -451,6 +453,7 @@ let cmdline_actions = "-dconstprop$", Set option_dconstprop; "-dcse$", Set option_dcse; "-dalloc$", Set option_dalloc; + "-dalloctrace$", Set option_dalloctrace; "-dmach$", Set option_dmach; "-dasm$", Set option_dasm; "-sdump$", Set option_sdump; |