From 7698300cfe2d3f944ce2e1d4a60a263620487718 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 20 Dec 2013 13:05:53 +0000 Subject: Merge of branch value-analysis. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Driver.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 5f0ae7e8..874f96b8 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -149,6 +149,7 @@ 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 PrintRTL.destination_deadcode option_ddeadcode ".deadcode.rtl"; set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest PrintLTL.destination option_dalloc ".alloc.ltl"; set_dest PrintMach.destination option_dmach ".mach"; @@ -413,6 +414,7 @@ Tracing options: -dinlining Save RTL after inlining optimization in .inlining.rtl -dconstprop Save RTL after constant propagation in .constprop.rtl -dcse Save RTL after CSE optimization in .cse.rtl + -ddeadcode Save RTL after dead code removal in .deadcode.rtl -dalloc Save LTL after register allocation in .alloc.ltl -dmach Save generated Mach code in .mach -dasm Save generated assembly in .s @@ -460,6 +462,7 @@ let cmdline_actions = "-dinlining$", Set option_dinlining; "-dconstprop$", Set option_dconstprop; "-dcse$", Set option_dcse; + "-ddeadcode$", Set option_ddeadcode; "-dalloc$", Set option_dalloc; "-dalloctrace$", Set option_dalloctrace; "-dmach$", Set option_dmach; -- cgit