From 92b6c68cdfd1e42ca1f9ebf70b7292e7c16570c2 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 19 Oct 2023 18:21:00 +0100
Subject: Finished most of the giblesubpar proof

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

(limited to 'driver/VericertDriver.ml')

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 5950e95..6cd8e1f 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -67,6 +67,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
   set_dest Vericert.PrintGibleSeq.destination option_dgblseq ".gblseq";
   set_dest Vericert.PrintGiblePar.destination option_dgblpar ".gblpar";
+  set_dest Vericert.PrintGibleSubPar.destination option_dgblsubpar ".gblsubpar";
   set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
   set_dest Vericert.PrintDHTL.destination option_ddhtl ".dhtl";
   set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
@@ -270,6 +271,7 @@ HLS Optimisations:
   -drtl          Save RTL at various optimization points in <file>.rtl.<n>
   -dgblseq       Save GibleSeq <file>.gblseq
   -dgblpar       Save GiblePar <file>.gblpar
+  -dgblsubpar    Save GibleSubPar <file>.gblsubpar
   -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
@@ -412,6 +414,7 @@ let cmdline_actions =
     option_drtl := true;
     option_dgblseq := true;
     option_dgblpar := true;
+    option_dgblsubpar := true;
     option_dhtl := true;
     option_ddhtl := true;
     option_dltl := true;
-- 
cgit