diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-06-05 22:42:28 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-05 22:42:28 +0100 |
| commit | 48d907ee56b39e7a8819700ae8a88af05c1b031e (patch) | |
| tree | 0d9cddc5622e5b9953b871908195aa606b3dd748 /src/hls/CondElim.v | |
| parent | 2e731050c69c98142d29d87fb863f199d50dfe19 (diff) | |
| download | vericert-48d907ee56b39e7a8819700ae8a88af05c1b031e.tar.gz vericert-48d907ee56b39e7a8819700ae8a88af05c1b031e.zip | |
Fix many more lemmas
Diffstat (limited to 'src/hls/CondElim.v')
| -rw-r--r-- | src/hls/CondElim.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/hls/CondElim.v b/src/hls/CondElim.v index b9bd1e9..9f51053 100644 --- a/src/hls/CondElim.v +++ b/src/hls/CondElim.v @@ -28,6 +28,8 @@ Require Import vericert.hls.GibleSeq. Require Import vericert.hls.Predicate. Require Import vericert.bourdoncle.Bourdoncle. +#[local] Open Scope positive. + Definition elim_cond_s (fresh: predicate) (i: instr) := match i with | RBexit p (RBcond c args n1 n2) => @@ -61,7 +63,7 @@ Definition elim_cond_fold (state: predicate * PTree.t SeqBB.t) (n: node) (b: Seq Definition transf_function (f: function) : function := mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) - (snd (PTree.fold elim_cond_fold f.(fn_code) (1%positive, PTree.empty _))) + (snd (PTree.fold elim_cond_fold f.(fn_code) (max_pred_function f + 1, PTree.empty _))) f.(fn_entrypoint). Definition transf_fundef (fd: fundef) : fundef := |