aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgen.v
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2018-12-11 16:44:42 +0100
committerCyril SIX <cyril.six@kalray.eu>2018-12-11 16:44:42 +0100
commitac666e83b2d4d41fa193aef4f81233e3d5735506 (patch)
tree7661508f8dd72d5fc66335b9607adc0c54c67b30 /mppa_k1c/Asmblockgen.v
parent51a27f176b0eb5fb2943807a5cb95f2024420936 (diff)
downloadcompcert-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.v26
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 =>