diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:50:50 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:50:50 +0100 |
| commit | b7bf754fce5e9442c3a5b1e5cec25ed522d0e870 (patch) | |
| tree | 267a432dbd7fe3102b2ce5278d72961b16f82366 /backend/CSE3analysis.v | |
| parent | 8c8e6a0528a91420e399ae84ccf293c0d8be285f (diff) | |
| download | compcert-kvx-b7bf754fce5e9442c3a5b1e5cec25ed522d0e870.tar.gz compcert-kvx-b7bf754fce5e9442c3a5b1e5cec25ed522d0e870.zip | |
oper sound
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 7 |
1 files changed, 3 insertions, 4 deletions
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. |