diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 11:45:36 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 11:45:36 +0100 |
| commit | 215d550f2154ae39506a19ee440cf7248367ea0a (patch) | |
| tree | 7cf915d58119f9fb3f5c3c0164a96204c047b5c9 | |
| parent | 01d6766f71067fb3490bcf3d05a3e0f60b6d0b14 (diff) | |
| download | compcert-kvx-215d550f2154ae39506a19ee440cf7248367ea0a.tar.gz compcert-kvx-215d550f2154ae39506a19ee440cf7248367ea0a.zip | |
PrintRTLblock
| -rw-r--r-- | driver/Compiler.v | 2 | ||||
| -rw-r--r-- | extraction/extraction.v | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 2d50baf5..dc809490 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -79,6 +79,7 @@ Require Import Compopts. Parameter print_Clight: Clight.program -> unit. Parameter print_Cminor: Cminor.program -> unit. Parameter print_RTL: Z -> RTL.program -> unit. +Parameter print_RTLblock: Z -> RTLblock.program -> unit. Parameter print_LTL: LTL.program -> unit. Parameter print_Mach: Mach.program -> unit. @@ -139,6 +140,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 8) @@@ time "To RTLblock" RTLblockgen.transl_program + @@ print (print_RTLblock 0) @@@ time "Back from RTLblock" RTLblockrevgen.transl_program @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program diff --git a/extraction/extraction.v b/extraction/extraction.v index 265a5967..8dbec209 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -133,6 +133,7 @@ Extract Constant Compopts.optim_coalesce_mem => Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". +Extract Constant Compiler.print_RTLblock => "PrintRTLblock.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". |