aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-02-22 18:41:33 +0000
committerYann Herklotz <git@yannherklotz.com>2021-02-22 18:41:33 +0000
commit91b62a7100ccb1f8910422bc4566bc57ade8f7e7 (patch)
tree5987436a23f446a42672061b7d8740b3a2775403 /driver
parenta5ae227155f09822207c49d75fdbb6e4b7652936 (diff)
downloadvericert-91b62a7100ccb1f8910422bc4566bc57ade8f7e7.tar.gz
vericert-91b62a7100ccb1f8910422bc4566bc57ade8f7e7.zip
Add RTLPar printing
Diffstat (limited to 'driver')
-rw-r--r--driver/VericertDriver.ml11
1 files changed, 7 insertions, 4 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index d2c301f..4c1e2f9 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";
@@ -390,6 +391,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;
@@ -403,6 +405,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;
@@ -417,10 +420,10 @@ let cmdline_actions =
warning_options @
(* Vericert.Interpreter mode *)
[ Exact "-interp", Set option_interp;
- Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0);
- Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2);
- Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random);
- Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.All)
+ Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0);
+ Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2);
+ Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random);
+ Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.All)
]
(* Optimization options *)
(* -f options: come in -f and -fno- variants *)