aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-10-18 18:14:52 +0100
committerYann Herklotz <git@yannherklotz.com>2020-10-18 18:14:52 +0100
commitf7e9951c08ac658537811d214c88d855a7e2c907 (patch)
treecbb29c2456e2d026f13ab3a7b26e45ede9fa73b9
parent0b1ce1ce5cde086bc67a428d69eee52c865ef1a5 (diff)
downloadvericert-kvx-f7e9951c08ac658537811d214c88d855a7e2c907.tar.gz
vericert-kvx-f7e9951c08ac658537811d214c88d855a7e2c907.zip
Add renumbering to compiler passes
-rw-r--r--src/Compiler.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Compiler.v b/src/Compiler.v
index 7a99bdb..ff8c523 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -109,6 +109,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res RTLBlock.program :=
@@@ Cminorgen.transl_program
@@@ Selection.sel_program
@@@ RTLgen.transl_program
+ @@ Renumber.transf_program
@@ print (print_RTL 0)
@@@ RTLBlockgen.transl_program.