diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-06 14:09:54 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-06 14:09:54 +0100 |
| commit | 78e549331ba3f136ebe94955f68767bd384df454 (patch) | |
| tree | e82c58fc59b6b4b1e9472cf26ce35ce0e6efdf14 /src/Compiler.v | |
| parent | c76ac9be323e3513aa0db2721ecd0f6c3987aef0 (diff) | |
| download | vericert-78e549331ba3f136ebe94955f68767bd384df454.tar.gz vericert-78e549331ba3f136ebe94955f68767bd384df454.zip | |
HTLgenproof compiles again
- Commented out Iload, Istore proofs for now
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index a34b359..17d8921 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -48,7 +48,9 @@ From compcert.driver Require From coqup Require Verilog Veriloggen - HTLgen. + Veriloggenproof + HTLgen + HTLgenproof. Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: HTL.program -> unit. @@ -107,6 +109,9 @@ Definition CompCert's_passes := ::: mkpass Cminorgenproof.match_prog ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog + ::: mkpass Inliningproof.match_prog + ::: mkpass HTLgenproof.match_prog + ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. Definition match_prog: Csyntax.program -> RTL.program -> Prop := |