diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 14:32:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 14:32:06 +0200 |
| commit | 138f4fb80d3dc6cce396dc57e64c28dc949ab94a (patch) | |
| tree | dbd40874c6ca5b74b1063b3140193ce3c3473b1d /mppa_k1c/Asm.v | |
| parent | 9dadf82c52a9ad11b31b21986bc88a108b845d0b (diff) | |
| download | compcert-kvx-138f4fb80d3dc6cce396dc57e64c28dc949ab94a.tar.gz compcert-kvx-138f4fb80d3dc6cce396dc57e64c28dc949ab94a.zip | |
removed fake ops for int32 -> double
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 53747851..d1ac8a67 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -149,9 +149,7 @@ Inductive instruction : Type := | Pfloatwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (32 -> 32) *)
| Pfloatuwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (u32 -> 32) *)
| Pfloatudrnsz (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (64 bits) *)
- | Pfloatudrnsz_i32 (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (32 bits) *)
| 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) *)
@@ -309,8 +307,6 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmvliw.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs
| PArithRR Asmvliw.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs
| PArithRR Asmvliw.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs
- | PArithRR Asmvliw.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs
- | PArithRR Asmvliw.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs
| PArithRR Asmvliw.Pfixedwrzz rd rs => Pfixedwrzz rd rs
| PArithRR Asmvliw.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs
| PArithRR Asmvliw.Pfixeddrzz rd rs => Pfixeddrzz rd rs
|