diff options
| author | Léo Gourdin <leo.gourdin@lilo.org> | 2021-07-28 17:00:02 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@lilo.org> | 2021-07-28 17:00:02 +0200 |
| commit | 92cca153569e44cd11ba3d1b68c2708c0cc46899 (patch) | |
| tree | 990c58ee9a15db32a6c87a8135295092433beb72 /scheduling/BTLmatchRTL.v | |
| parent | 23569a795598f18cad851f1bda39dd1a2e630ded (diff) | |
| download | compcert-kvx-92cca153569e44cd11ba3d1b68c2708c0cc46899.tar.gz compcert-kvx-92cca153569e44cd11ba3d1b68c2708c0cc46899.zip | |
ci fix?
Diffstat (limited to 'scheduling/BTLmatchRTL.v')
| -rw-r--r-- | scheduling/BTLmatchRTL.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v index c271ae02..07131893 100644 --- a/scheduling/BTLmatchRTL.v +++ b/scheduling/BTLmatchRTL.v @@ -214,9 +214,9 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i | mib_op isfst pc pc' op lr r iinfo: cfg!pc = Some (Iop op lr r pc') -> match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc') - | mib_load isfst pc pc' m a lr r iinfo: - cfg!pc = Some (Iload TRAP m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc') + | mib_load isfst pc pc' trap m a lr r iinfo: + cfg!pc = Some (Iload trap m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bload trap m a lr r iinfo) (Some pc') | mib_store isfst pc pc' m a lr r iinfo: cfg!pc = Some (Istore m a lr r pc') -> match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc') @@ -407,7 +407,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | Bload tm m a lr r _ => match cfg!pc with | Some (Iload tm' m' a' lr' r' pc') => - if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then + if (trapping_mode_eq tm tm') then if (chunk_eq m m') then if (eq_addressing a a') then if (list_eq_dec Pos.eq_dec lr lr') then @@ -417,7 +417,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different lr in Bload") else Error (msg "BTL.verify_block: different addressing in Bload") else Error (msg "BTL.verify_block: different chunk in Bload") - else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload") + else Error (msg "BTL.verify_block: different trapping_mode in Bload") | _ => Error (msg "BTL.verify_block: incorrect cfg Bload") end | Bstore m a lr r _ => @@ -520,8 +520,7 @@ Proof. constructor; assumption. - (* Bload *) destruct i; try discriminate. - do 2 (destruct (trapping_mode_eq _ _); try discriminate). - simpl in H. + destruct (trapping_mode_eq _ _); try discriminate. destruct (chunk_eq _ _); try discriminate. destruct (eq_addressing _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. |