diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 19:52:59 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 19:52:59 +0100 |
| commit | f8ff27915f8c4d5fb6f31ec2a0a73f65cf604c43 (patch) | |
| tree | e1186fac9de9c83ba0d0d0bc43bb9ac0fe86ef26 /driver | |
| parent | f26f3887d0b0ac286c317a5425a3a4781871cfc2 (diff) | |
| download | vericert-f8ff27915f8c4d5fb6f31ec2a0a73f65cf604c43.tar.gz vericert-f8ff27915f8c4d5fb6f31ec2a0a73f65cf604c43.zip | |
Add htl pretty printing
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/CoqupDriver.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml index afbe4d0..0b64f48 100644 --- a/driver/CoqupDriver.ml +++ b/driver/CoqupDriver.ml @@ -65,6 +65,7 @@ let compile_c_file sourcename ifile ofile = set_dest Coqup.PrintClight.destination option_dclight ".light.c"; set_dest Coqup.PrintCminor.destination option_dcminor ".cm"; set_dest Coqup.PrintRTL.destination option_drtl ".rtl"; + set_dest Coqup.PrintHTL.destination option_dhtl ".htl"; set_dest Coqup.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Coqup.PrintLTL.destination option_dltl ".ltl"; set_dest Coqup.PrintMach.destination option_dmach ".mach"; @@ -253,6 +254,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> + -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 -dasm Save generated assembly in <file>.s @@ -377,6 +379,7 @@ let cmdline_actions = Exact "-dclight", Set option_dclight; Exact "-dcminor", Set option_dcminor; Exact "-drtl", Set option_drtl; + Exact "-dhtl", Set option_dhtl; Exact "-dltl", Set option_dltl; Exact "-dalloctrace", Set option_dalloctrace; Exact "-dmach", Set option_dmach; @@ -388,6 +391,7 @@ let cmdline_actions = option_dclight := true; option_dcminor := true; option_drtl := true; + option_dhtl := true; option_dltl := true; option_dalloctrace := true; option_dmach := true; |