From b7bf754fce5e9442c3a5b1e5cec25ed522d0e870 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 10 Mar 2020 15:50:50 +0100 Subject: oper sound --- backend/CSE3analysis.v | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'backend/CSE3analysis.v') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index cdda2cb7..6cce52c7 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -245,14 +245,13 @@ Section OPERATIONS. | None => kill_reg dst rel end. - (* Definition oper (dst : reg) (op: sym_op) (args : list reg) (rel : RELATION.t) : RELATION.t := - match find_op rel op (forward_move_l rel args) with + match rhs_find op (forward_move_l rel args) rel with | Some r => move r dst rel - | None => oper1 op dst args rel + | None => oper1 dst op args rel end. -*) + End PER_NODE. End OPERATIONS. -- cgit