From 3fef5e1d45820a775a7c941851af6f0bf3f1537d Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 11 Mar 2020 17:00:48 +0100 Subject: Adding info field for branching in RTL, LTL, XTL and all associated passes --- backend/Duplicateproof.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'backend/Duplicateproof.v') 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') -- cgit