From 5cc780e10afa2851980fd3157644cccb1f528b1c Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 23 Oct 2020 13:25:32 +0100
Subject: Add printing of intermediate rtlblock language

---
 driver/VericertDriver.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'driver/VericertDriver.ml')

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 0362456..cb3ee8e 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -65,6 +65,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest Vericert.PrintClight.destination option_dclight ".light.c";
   set_dest Vericert.PrintCminor.destination option_dcminor ".cm";
   set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
+  set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock";
   set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
   set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
   set_dest Vericert.PrintLTL.destination option_dltl ".ltl";
@@ -254,6 +255,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
   -dclight       Save generated Clight in <file>.light.c
   -dcminor       Save generated Cminor in <file>.cm
   -drtl          Save RTL at various optimization points in <file>.rtl.<n>
+  -drtlblock     Save RTLBlock <file>.rtlblock
   -dhtl          Save HTL before Verilog generation <file>.htl
   -dltl          Save LTL after register allocation in <file>.ltl
   -dmach         Save generated Mach code in <file>.mach
@@ -379,6 +381,7 @@ let cmdline_actions =
   Exact "-dclight", Set option_dclight;
   Exact "-dcminor", Set option_dcminor;
   Exact "-drtl", Set option_drtl;
+  Exact "-drtlblock", Set option_drtlblock;
   Exact "-dhtl", Set option_dhtl;
   Exact "-dltl", Set option_dltl;
   Exact "-dalloctrace", Set option_dalloctrace;
@@ -391,6 +394,7 @@ let cmdline_actions =
     option_dclight := true;
     option_dcminor := true;
     option_drtl := true;
+    option_drtlblock := true;
     option_dhtl := true;
     option_dltl := true;
     option_dalloctrace := true;
-- 
cgit