diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-29 19:33:33 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-29 19:33:33 +0200 |
| commit | 51094cecd5d24023e3de2487e66765f8c54b5fcc (patch) | |
| tree | de1a40bdde10611736acebcd6124f99af1509a00 /mppa_k1c/Asmblockgen.v | |
| parent | 595db90221d4f45682ec5aaac0b485ff32af09e5 (diff) | |
| download | compcert-kvx-51094cecd5d24023e3de2487e66765f8c54b5fcc.tar.gz compcert-kvx-51094cecd5d24023e3de2487e66765f8c54b5fcc.zip | |
fmin/fmax/fminf/fmaxf non bien testés
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index e5b9b35a..1f3f7539 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -775,6 +775,18 @@ Definition transl_op | Omulfs, a1 :: a2 :: nil => do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; OK (Pfmulw rd rs1 rs2 ::i k) + | Ominf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmind rd rs1 rs2 ::i k) + | Ominfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfminw rd rs1 rs2 ::i k) + | Omaxf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmaxd rd rs1 rs2 ::i k) + | Omaxfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmaxw rd rs1 rs2 ::i k) | Onegf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; OK (Pfnegd rd rs ::i k) |