diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 12:29:17 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 12:29:17 +0100 |
| commit | 9526f710a65f9009822240bf2b47e9bc6c07cf19 (patch) | |
| tree | 7076de5f21e11f68b5907f01fc94828d68b44da2 | |
| parent | 456787ab7f394e15b3b0481f4d4178ebf04259c7 (diff) | |
| download | compcert-kvx-9526f710a65f9009822240bf2b47e9bc6c07cf19.tar.gz compcert-kvx-9526f710a65f9009822240bf2b47e9bc6c07cf19.zip | |
ValueAOp rotate 32-bit
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 5670b5fe..26a49135 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -73,6 +73,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshlimm n, v1::nil => shl v1 (I n) | Oshr, v1::v2::nil => shr v1 v2 | Oshrimm n, v1::nil => shr v1 (I n) + | Ororimm n, v1::nil => ror v1 (I n) | Oshru, v1::v2::nil => shru v1 v2 | Oshruimm n, v1::nil => shru v1 (I n) | Oshrximm n, v1::nil => shrx v1 (I n) |