diff options
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index a5c7f495..54bf247f 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -294,6 +294,7 @@ Inductive arith_name_rr : Type := | 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) *) | Pfixedudrzz (**r Integer conversion from floating point (float -> unsigned long) *) | Pfixeddrzz_i32 (**r Integer conversion from floating point (float -> int) *) @@ -948,6 +949,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | Pfloatdrnsz => rs#d <- (match Val.floatoflong rs#s with Some f => f | _ => Vundef end) | Pfloatdrnsz_i32 => rs#d <- (match Val.floatofint rs#s with Some f => f | _ => Vundef end) | Pfixedwrzz => rs#d <- (match Val.intofsingle rs#s with Some i => i | _ => Vundef end) + | Pfixeduwrzz => rs#d <- (match Val.intuofsingle rs#s with Some i => i | _ => Vundef end) | Pfixeddrzz => rs#d <- (match Val.longoffloat rs#s with Some i => i | _ => Vundef end) | Pfixeddrzz_i32 => rs#d <- (match Val.intoffloat rs#s with Some i => i | _ => Vundef end) | Pfixedudrzz => rs#d <- (match Val.longuoffloat rs#s with Some i => i | _ => Vundef end) |