diff options
Diffstat (limited to 'backend/ForwardMoves.v')
| -rw-r--r-- | backend/ForwardMoves.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index 0e71b6b5..660d0458 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -250,13 +250,14 @@ Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) := Definition apply_instr instr x := match instr with | Inop _ + | Icond _ _ _ _ | Istore _ _ _ _ _ => Some x | Iop Omove (src :: nil) dst _ => Some (move src dst x) | Iop _ _ dst _ | Iload _ _ _ _ dst _ | Icall _ _ _ dst _ => Some (kill dst x) | Ibuiltin _ _ res _ => Some (kill_builtin_res res x) - | Icond _ _ _ _ | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot + | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot end. Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := |