diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-10-18 18:14:52 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-10-18 18:14:52 +0100 |
| commit | f7e9951c08ac658537811d214c88d855a7e2c907 (patch) | |
| tree | cbb29c2456e2d026f13ab3a7b26e45ede9fa73b9 /src/Compiler.v | |
| parent | 0b1ce1ce5cde086bc67a428d69eee52c865ef1a5 (diff) | |
| download | vericert-f7e9951c08ac658537811d214c88d855a7e2c907.tar.gz vericert-f7e9951c08ac658537811d214c88d855a7e2c907.zip | |
Add renumbering to compiler passes
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 1 |
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. |