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/Asmblock.v | |
| parent | 50affca71434b1e1ca3e75ce8f62a304ed1913cf (diff) | |
| download | compcert-kvx-df32503f46a62b18f92363ac7f81ec0d5b36c64a.tar.gz compcert-kvx-df32503f46a62b18f92363ac7f81ec0d5b36c64a.zip | |
Ointuofsingle done
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) |