diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-15 13:13:43 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-15 13:14:15 +0100 |
| commit | 99532322330291ff6a2888af559d5df5028c7524 (patch) | |
| tree | 620828d8fcdd380628ed9f4a3865225cd7ff0554 /src/hls/GiblePargen.v | |
| parent | 1849816610419f688bddcb7446fd946995e3c2be (diff) | |
| download | vericert-99532322330291ff6a2888af559d5df5028c7524.tar.gz vericert-99532322330291ff6a2888af559d5df5028c7524.zip | |
Add example computation to update function
Diffstat (limited to 'src/hls/GiblePargen.v')
| -rw-r--r-- | src/hls/GiblePargen.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 0462e28..11da966 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -287,6 +287,17 @@ Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pr | 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 => + match update x (RBop None (Op.Ointconst (Int.repr 10)) nil 3) with + | Some y => + RTree.get (Reg 3) (forest_regs (snd y)) + | None => None + end + | None => None + end.*) + (*| Implementing which are necessary to show the correctness of the translation validation by showing that there aren't any more effects in the resultant RTLPar |