aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Deadcode.v
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-03-11 17:00:48 +0100
committerCyril SIX <cyril.six@kalray.eu>2020-03-11 17:00:48 +0100
commit3fef5e1d45820a775a7c941851af6f0bf3f1537d (patch)
treefc36893a6d590f33bd21ab40e040143793998eaa /backend/Deadcode.v
parent1b00a75796a8ace42cc480efadaad948407f5a31 (diff)
downloadcompcert-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/Deadcode.v')
-rw-r--r--backend/Deadcode.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index 1f208a91..3412a6fa 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -142,7 +142,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t)
nmem_dead_stack f.(fn_stacksize))
| Some(Ibuiltin ef args res s) =>
transfer_builtin approx!!pc ef args res ne nm
- | Some(Icond cond args s1 s2) =>
+ | Some(Icond cond args s1 s2 _) =>
if peq s1 s2 then after else
(add_needs args (needs_of_condition cond) ne, nm)
| Some(Ijumptable arg tbl) =>
@@ -192,7 +192,7 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t)
if nmem_contains (snd an!!pc) (aaddr_arg approx!!pc dst) sz
then instr
else Inop s
- | Icond cond args s1 s2 =>
+ | Icond cond args s1 s2 _ =>
if peq s1 s2 then Inop s1 else instr
| _ =>
instr