aboutsummaryrefslogtreecommitdiffstats
path: root/driver/VericertDriver.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/VericertDriver.ml')
-rw-r--r--driver/VericertDriver.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 0706d79..a36f375 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -66,6 +66,7 @@ let compile_c_file sourcename ifile ofile =
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.PrintRTLPar.destination option_drtlpar ".rtlpar";
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";
@@ -391,6 +392,7 @@ let cmdline_actions =
Exact "-dcminor", Set option_dcminor;
Exact "-drtl", Set option_drtl;
Exact "-drtlblock", Set option_drtlblock;
+ Exact "-drtlpar", Set option_drtlpar;
Exact "-dhtl", Set option_dhtl;
Exact "-dltl", Set option_dltl;
Exact "-dalloctrace", Set option_dalloctrace;
@@ -404,6 +406,7 @@ let cmdline_actions =
option_dcminor := true;
option_drtl := true;
option_drtlblock := true;
+ option_drtlpar := true;
option_dhtl := true;
option_dltl := true;
option_dalloctrace := true;