diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-02 18:30:25 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-02 18:30:25 +0200 |
| commit | 71c58a8d494eafd847776446b0c246229b2bc9cf (patch) | |
| tree | 7570087588f24b3b340baeed5871b398bf7fc390 /backend/Deadcode.v | |
| parent | dc8b24fa2dd7ede561dd75458899cf42e9be09d2 (diff) | |
| download | compcert-kvx-71c58a8d494eafd847776446b0c246229b2bc9cf.tar.gz compcert-kvx-71c58a8d494eafd847776446b0c246229b2bc9cf.zip | |
avancement (il faut utiliser Vundef visiblement)
Diffstat (limited to 'backend/Deadcode.v')
| -rw-r--r-- | backend/Deadcode.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 |