diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 14:07:07 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 14:07:07 +0100 |
| commit | 983cab07c39a7bed288e9e953d95ffe990783825 (patch) | |
| tree | 6f797df094b2b0299ddd4b83af5ce3395829800b /mppa_k1c/Asmblockgen.v | |
| parent | 29d5c75e65a7fddf88bbd8c1946e700eed09dd23 (diff) | |
| download | compcert-kvx-983cab07c39a7bed288e9e953d95ffe990783825.tar.gz compcert-kvx-983cab07c39a7bed288e9e953d95ffe990783825.zip | |
32-bit rotate finished
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 1c176538..26b1c6c1 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -471,7 +471,10 @@ Definition transl_op Psrliw RTMP RTMP (Int.sub Int.iwordsize n) ::i Paddw RTMP rs RTMP ::i Psraiw rd RTMP n ::i k) - + | Ororimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Proriw rd rs n ::i k) + (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; |