aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgen.v
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2019-02-12 16:47:18 +0100
committerCyril SIX <cyril.six@kalray.eu>2019-02-12 16:47:18 +0100
commit685c2f76b5f8b320495868cfdcadbf203f50a0bd (patch)
treede1e379c6c99cdc94ecaf930318c79718dcce9cb /mppa_k1c/Asmblockgen.v
parent41109bd86942b028240ac20758ff29853b025534 (diff)
downloadcompcert-kvx-685c2f76b5f8b320495868cfdcadbf203f50a0bd.tar.gz
compcert-kvx-685c2f76b5f8b320495868cfdcadbf203f50a0bd.zip
Added Ointofsingle + floatconv unit test
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
-rw-r--r--mppa_k1c/Asmblockgen.v5
1 files changed, 4 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 07051111..80790465 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -548,8 +548,11 @@ Definition transl_op
do rd <- freg_of res; do rs <- freg_of a1;
OK (Pfnegd rd rs ::i k)
| Osingleofint, a1 :: nil =>
- do rd <- freg_of res; do rs <- freg_of a1;
+ do rd <- freg_of res; do rs <- ireg_of a1;
OK (Pfloatwrnsz rd rs ::i k)
+ | Ointofsingle, a1 :: nil =>
+ do rd <- ireg_of res; do rs <- freg_of a1;
+ OK (Pfixedwrzz rd rs ::i k)
| Oabsf , _ => Error (msg "Asmblockgen.transl_op: Oabsf")
| Oaddf , _ => Error (msg "Asmblockgen.transl_op: Oaddf")
| Osubf , _ => Error (msg "Asmblockgen.transl_op: Osubf")