diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 14:42:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 14:42:03 +0100 |
| commit | fc4bc25ca5d986831a02cddd87264b7b51943fc4 (patch) | |
| tree | 075f6cf97f3a35a0c6d34650806b295573288c5f /src/hls/GiblePargen.v | |
| parent | 28352e0b7c53f7b0d3e610bf8507ee4b0901171d (diff) | |
| download | vericert-fc4bc25ca5d986831a02cddd87264b7b51943fc4.tar.gz vericert-fc4bc25ca5d986831a02cddd87264b7b51943fc4.zip | |
Prove evaluable_pred_expr_exists_RBsetpred
Diffstat (limited to 'src/hls/GiblePargen.v')
| -rw-r--r-- | src/hls/GiblePargen.v | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 08806aa..91b0450 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -279,16 +279,6 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest Some (new_p, f <-e pruned) end. -Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr := - match i with - | RBnop => lst - | RBop p op rl r => (f #r (Reg r)) :: lst - | RBload p chunk addr rl r => (f #r (Reg r)) :: lst - | RBstore p chunk addr rl r => (f #r Mem) :: lst - | RBsetpred p' c args p => lst - | RBexit p c => lst - end. - (*Compute match update (T, mk_forest (PTree.empty _) (PTree.empty _) (NE.singleton (T, EEbase))) (RBop None Op.Odiv (1::2::nil) 3) with | Some x => |