diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-21 18:57:33 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-21 18:57:33 +0100 |
| commit | 4d262face34cb79d478823fd8db32cf02dc187f8 (patch) | |
| tree | 820335def3dc6d2fda3b779e8079b0c5fac8620c /src/Compiler.v | |
| parent | 323f262727ac3a4b129bdaeaa21083d8daa5184c (diff) | |
| download | vericert-4d262face34cb79d478823fd8db32cf02dc187f8.tar.gz vericert-4d262face34cb79d478823fd8db32cf02dc187f8.zip | |
Add SMTCoq solver as dependency
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 5ff291e..2fb909e 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -55,6 +55,7 @@ Require Import compcert.common.Errors. Require Import compcert.common.Linking. Require Import compcert.common.Smallstep. Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Maps. Require vericert.hls.Verilog. Require vericert.hls.Veriloggen. @@ -279,7 +280,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_GibleSeq 0) @@ total_if HLSOpts.optim_if_conversion CondElim.transf_program @@ print (print_GibleSeq 1) - @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (Maps.PTree.empty _ :: Maps.PTree.empty _ :: nil)) + @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (PTree.empty _ :: PTree.empty _ :: nil)) @@ print (print_GibleSeq 2) @@@ DeadBlocks.transf_program @@ print (print_GibleSeq 3) |