diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-17 13:45:42 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-17 13:45:42 +0100 |
commit | 1848a8f4c08ef55a045d4dc1e78f517182a50442 (patch) | |
tree | bc1d3147c2db76b962c8fa3682ac5dd1e4e6cd3a /mppa_k1c/Asmblockgen.v | |
parent | 15c5ca037eabb9891f7880bc2d517982ba34e769 (diff) | |
parent | fe3fc2fd3d5a312ac526c5596e851e315782d9f6 (diff) | |
download | compcert-kvx-1848a8f4c08ef55a045d4dc1e78f517182a50442.tar.gz compcert-kvx-1848a8f4c08ef55a045d4dc1e78f517182a50442.zip |
Merge branch 'mppa_k1c' into mppa_postpass
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index a4d0526d..9a564117 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -398,19 +398,19 @@ Definition transl_op | Omulhu, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmulhuw rd rs1 rs2 :: k) - | Odiv, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivw rd rs1 rs2 :: k) - | Odivu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivuw rd rs1 rs2 :: k) - | Omod, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premw rd rs1 rs2 :: k) - | Omodu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premuw rd rs1 rs2 :: k) -*)| Oand, a1 :: a2 :: nil => +*)| Odiv, a1 :: a2 :: nil => Error(msg "32-bits division not supported yet. Please use 64-bits.") + (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pdivw rd rs1 rs2 :: k) *) + | Odivu, a1 :: a2 :: nil => Error(msg "32-bits division not supported yet. Please use 64-bits.") + (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pdivuw rd rs1 rs2 :: k) *) + | Omod, a1 :: a2 :: nil => Error(msg "32-bits modulo not supported yet. Please use 64-bits.") + (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Premw rd rs1 rs2 :: k) *) + | Omodu, a1 :: a2 :: nil => Error(msg "32-bits modulo not supported yet. Please use 64-bits.") + (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Premuw rd rs1 rs2 :: k) *) + | Oand, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandw rd rs1 rs2 ::i k) | Oandimm n, a1 :: nil => |