diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-05-31 02:05:17 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-31 02:05:17 +0100 |
| commit | d90473f74c93a22bdecdef6057f5efccfa465e65 (patch) | |
| tree | 9efb3da621b0c75d77c71f72bbc3dd7d46dc8a8b /src | |
| parent | 2d4be10eeadcbb6aa4cc3d48e596dfc500a0d773 (diff) | |
| download | vericert-d90473f74c93a22bdecdef6057f5efccfa465e65.tar.gz vericert-d90473f74c93a22bdecdef6057f5efccfa465e65.zip | |
Fix update function for control-flow
Diffstat (limited to 'src')
| -rw-r--r-- | src/hls/GiblePargen.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 0d4badd..3ccb765 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -169,6 +169,17 @@ of the expression to the other predicates. Definition forest_state : Type := forest * list (cf_instr * option pred_op * forest). +Definition upd_pred_forest (p: option pred_op) (f: forest) := + match p with + | Some p' => + PTree.map (fun i e => + NE.map (fun (x: pred_op * expression) => + let (pred, expr) := x in + (Pand p' pred, expr) + ) e) f + | None => f + end. + Definition update (flist : forest_state) (i : instr): forest_state := let (f, fl) := flist in match i with @@ -201,7 +212,7 @@ Definition update (flist : forest_state) (i : instr): forest_state := (f # (Pred p)) (map_predicated (pred_ret (Esetpred c)) (merge (list_translation args f)))), fl) - | RBexit p c => (f, (c, p, f) :: fl) + | RBexit p c => ((upd_pred_forest (option_map negate p) f), (c, p, upd_pred_forest p f) :: fl) end. (*| |