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/Asmvliw.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/Asmvliw.v')
-rw-r--r-- | mppa_k1c/Asmvliw.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 3f2179c2..cf827818 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -322,9 +322,7 @@ Inductive arith_name_rr : Type := | Pfloatwrnsz (**r Floating Point conversion from integer (int -> SINGLE) *) | Pfloatuwrnsz (**r Floating Point conversion from integer (unsigned int -> SINGLE) *) | Pfloatudrnsz (**r Floating Point Conversion from integer (unsigned long -> float) *) - | Pfloatudrnsz_i32 (**r Floating Point Conversion from integer (unsigned int -> float) *) | Pfloatdrnsz (**r Floating Point Conversion from integer (long -> float) *) - | Pfloatdrnsz_i32 (**r Floating Point Conversion from integer (int -> float) *) | Pfixedwrzz (**r Integer conversion from floating point (single -> int) *) | Pfixeduwrzz (**r Integer conversion from floating point (single -> unsigned int) *) | Pfixeddrzz (**r Integer conversion from floating point (float -> long) *) @@ -909,8 +907,6 @@ Definition arith_eval_rr n v := | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end - | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end - | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end |