diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 16:47:18 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 16:47:18 +0100 |
| commit | 685c2f76b5f8b320495868cfdcadbf203f50a0bd (patch) | |
| tree | de1e379c6c99cdc94ecaf930318c79718dcce9cb /mppa_k1c/Asmblock.v | |
| parent | 41109bd86942b028240ac20758ff29853b025534 (diff) | |
| download | compcert-kvx-685c2f76b5f8b320495868cfdcadbf203f50a0bd.tar.gz compcert-kvx-685c2f76b5f8b320495868cfdcadbf203f50a0bd.zip | |
Added Ointofsingle + floatconv unit test
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index fbc9a5c6..643870ea 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -283,7 +283,8 @@ Inductive arith_name_rr : Type := | Pcvtl2w (**r Convert Long to Word *) | Psxwd (**r Sign Extend Word to Double Word *) | Pzxwd (**r Zero Extend Word to Double Word *) - | Pfloatwrnsz (**r Floating Point Conversion from integer *) + | Pfloatwrnsz (**r Floating Point Conversion from integer (single -> int) *) + | Pfixedwrzz (**r Integer conversion from floating point (int -> single) *) . Inductive arith_name_ri32 : Type := @@ -886,6 +887,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | Psxwd => rs#d <- (Val.longofint rs#s) | Pzxwd => rs#d <- (Val.longofintu rs#s) | Pfloatwrnsz => rs#d <- (match Val.singleofint rs#s with Some f => f | _ => Vundef end) + | Pfixedwrzz => rs#d <- (match Val.intofsingle rs#s with Some i => i | _ => Vundef end) end | PArithRI32 n d i => |