aboutsummaryrefslogtreecommitdiffstats
path: root/driver/VericertDriver.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-29 22:03:06 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-29 22:03:06 +0100
commit5d42b5fc8b24492f4457ccd541751db869fefc20 (patch)
treedb3b7aaf01b76cd55e9d490dcbf40ebec84508f9 /driver/VericertDriver.ml
parentbb5695f5bcb9f3c3c7948c0f3a36da55ba5dcbcf (diff)
parentab1e748f622f4345a3fc13ebbdbc8f223bd10e5c (diff)
downloadvericert-kvx-5d42b5fc8b24492f4457ccd541751db869fefc20.tar.gz
vericert-kvx-5d42b5fc8b24492f4457ccd541751db869fefc20.zip
Merge remote-tracking branch 'origin/develop' into develop
Diffstat (limited to 'driver/VericertDriver.ml')
-rw-r--r--driver/VericertDriver.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 1ea580f..aa5309a 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";