From 71c58a8d494eafd847776446b0c246229b2bc9cf Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Sep 2019 18:30:25 +0200 Subject: avancement (il faut utiliser Vundef visiblement) --- backend/Deadcode.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/Deadcode.v') diff --git a/backend/Deadcode.v b/backend/Deadcode.v index 2286876e..1f208a91 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -123,7 +123,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) if is_dead nres then after else if is_int_zero nres then (kill res ne, nm) else (add_needs args (needs_of_operation op nres) (kill res ne), nm) - | Some (Iload chunk addr args dst s) => + | Some (Iload trap chunk addr args dst s) => let ndst := nreg ne dst in if is_dead ndst then after else if is_int_zero ndst then (kill dst ne, nm) @@ -175,7 +175,7 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t) end else instr - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => let ndst := nreg (fst an!!pc) dst in if is_dead ndst then Inop s -- cgit