aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/NeedOp.v
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-16 11:00:56 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-16 11:00:56 +0100
commit456787ab7f394e15b3b0481f4d4178ebf04259c7 (patch)
treebb60e8ec5ff950a49a4cafa9264000be1c0747e3 /mppa_k1c/NeedOp.v
parentfbe5ac2c9619441ad84dedf3c0cdabb315f9f974 (diff)
downloadcompcert-kvx-456787ab7f394e15b3b0481f4d4178ebf04259c7.tar.gz
compcert-kvx-456787ab7f394e15b3b0481f4d4178ebf04259c7.zip
instruction rotate
Diffstat (limited to 'mppa_k1c/NeedOp.v')
-rw-r--r--mppa_k1c/NeedOp.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 117bbcb4..28d60fa5 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -54,6 +54,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Oshl | Oshr | Oshru => op2 (default nv)
| Oshlimm n => op1 (shlimm nv n)
| Oshrimm n => op1 (shrimm nv n)
+ | Ororimm n => op1 (ror nv n)
| Oshruimm n => op1 (shruimm nv n)
| Oshrximm n => op1 (default nv)
| Omakelong => op2 (default nv)