diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-01 14:44:09 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-01 14:44:09 +0100 |
| commit | df32503f46a62b18f92363ac7f81ec0d5b36c64a (patch) | |
| tree | b11b1282e4b44e96c84dcaad438ee4e264fcacc9 /mppa_k1c/Asm.v | |
| parent | 50affca71434b1e1ca3e75ce8f62a304ed1913cf (diff) | |
| download | compcert-kvx-df32503f46a62b18f92363ac7f81ec0d5b36c64a.tar.gz compcert-kvx-df32503f46a62b18f92363ac7f81ec0d5b36c64a.zip | |
Ointuofsingle done
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d930b168..dcce98d0 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -110,6 +110,7 @@ Inductive instruction : Type := | Pfloatdrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (64 bits) *)
| Pfloatdrnsz_i32 (rd rs: ireg) (**r Floating Point Conversion from integer (32 bits) *)
| Pfixedwrzz (rd rs: ireg) (**r Integer conversion from floating point *)
+ | Pfixeduwrzz (rd rs: ireg) (**r Integer conversion from floating point (f32 -> 32 bits unsigned *)
| Pfixeddrzz (rd rs: ireg) (**r Integer conversion from floating point (i64 -> 64 bits) *)
| Pfixeddrzz_i32 (rd rs: ireg) (**r Integer conversion from floating point (i32 -> f64) *)
| Pfixedudrzz (rd rs: ireg) (**r unsigned Integer conversion from floating point (u64 -> 64 bits) *)
@@ -229,6 +230,7 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmblock.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs
| PArithRR Asmblock.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs
| PArithRR Asmblock.Pfixedwrzz rd rs => Pfixedwrzz rd rs
+ | PArithRR Asmblock.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs
| PArithRR Asmblock.Pfixeddrzz rd rs => Pfixeddrzz rd rs
| PArithRR Asmblock.Pfixedudrzz rd rs => Pfixedudrzz rd rs
| PArithRR Asmblock.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs
|