diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-03-11 17:00:48 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-03-11 17:00:48 +0100 |
| commit | 3fef5e1d45820a775a7c941851af6f0bf3f1537d (patch) | |
| tree | fc36893a6d590f33bd21ab40e040143793998eaa /backend/Duplicateproof.v | |
| parent | 1b00a75796a8ace42cc480efadaad948407f5a31 (diff) | |
| download | compcert-kvx-3fef5e1d45820a775a7c941851af6f0bf3f1537d.tar.gz compcert-kvx-3fef5e1d45820a775a7c941851af6f0bf3f1537d.zip | |
Adding info field for branching in RTL, LTL, XTL and all associated passes
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 466b4b75..6b598dc7 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -23,12 +23,12 @@ Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop match_inst dupmap (Itailcall s ri lr) (Itailcall s ri lr) | match_inst_builtin: forall n n' ef la br, dupmap!n' = (Some n) -> match_inst dupmap (Ibuiltin ef la br n) (Ibuiltin ef la br n') - | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr, + | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr i i', dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) -> - match_inst dupmap (Icond c lr ifso ifnot) (Icond c lr ifso' ifnot') - | match_inst_revcond: forall ifso ifso' ifnot ifnot' c lr, + match_inst dupmap (Icond c lr ifso ifnot i) (Icond c lr ifso' ifnot' i') + | match_inst_revcond: forall ifso ifso' ifnot ifnot' c lr i i', dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) -> - match_inst dupmap (Icond c lr ifso ifnot) (Icond (negate_condition c) lr ifnot' ifso') + match_inst dupmap (Icond c lr ifso ifnot i) (Icond (negate_condition c) lr ifnot' ifso' i') | match_inst_jumptable: forall ln ln' r, list_forall2 (fun n n' => (dupmap!n' = (Some n))) ln ln' -> match_inst dupmap (Ijumptable r ln) (Ijumptable r ln') |