diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 15:58:34 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 15:58:34 +0100 |
| commit | 15184c16b3c560108d0ec28feceae13ffaaca959 (patch) | |
| tree | 9f5bb5524aa4163692a22c0da41fdd5c9c253e22 /mppa_k1c/Asmblockgen.v | |
| parent | 88448ee297d8894ecfb09d7925663cf6eb12cf01 (diff) | |
| parent | c5836e2d5f6a7183db97905040376f68459ad465 (diff) | |
| download | compcert-kvx-15184c16b3c560108d0ec28feceae13ffaaca959.tar.gz compcert-kvx-15184c16b3c560108d0ec28feceae13ffaaca959.zip | |
Merge branch 'mppa-mul' into mppa-jumptable
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index f3b4b921..1afb627a 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -425,18 +425,6 @@ Definition transl_op OK (mulimm32 rd rs1 n ::i k) | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") (* Normalement pas émis *) | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") (* Normalement pas émis *) - | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 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 "Asmblockgen.transl_op: Odivu: 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 "Asmblockgen.transl_op: Omod: 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 "Asmblockgen.transl_op: Omodu: 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) |