From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: 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 --- driver/Driver.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 3a5981eb..eb0e004a 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; -- cgit