diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-12-11 16:44:42 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-12-11 16:44:42 +0100 |
commit | ac666e83b2d4d41fa193aef4f81233e3d5735506 (patch) | |
tree | 7661508f8dd72d5fc66335b9607adc0c54c67b30 /mppa_k1c/Asmblockgen.v | |
parent | 51a27f176b0eb5fb2943807a5cb95f2024420936 (diff) | |
download | compcert-kvx-ac666e83b2d4d41fa193aef4f81233e3d5735506.tar.gz compcert-kvx-ac666e83b2d4d41fa193aef4f81233e3d5735506.zip |
Added an error message for 32-bits division and modulo
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 8bcbc712..2d345fe0 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 => |