diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 15:26:03 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 15:26:03 +0200 |
| commit | a6c79438ae754d969558bd37eb3a7676be6e66aa (patch) | |
| tree | 18f70fc6ef416e53638c445fa8ca745aef0b0fe1 /mppa_k1c/Asm.v | |
| parent | 5e35117f8dd7cc4c548ecd704e11f3ca8845dedd (diff) | |
| download | compcert-kvx-a6c79438ae754d969558bd37eb3a7676be6e66aa.tar.gz compcert-kvx-a6c79438ae754d969558bd37eb3a7676be6e66aa.zip | |
MPPA - Ocast32signed
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index db2f9ee2..d7007102 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -209,6 +209,8 @@ Inductive instruction : Type := (** Conversions *) | Pcvtl2w (rd: ireg) (rs: ireg) (**r Convert Long to Word *) + | Pcvtw2l (r : ireg) (**r Convert Word to Long *) + | Pmvw2l (rd: ireg) (rs: ireg) (**r Move Convert Word to Long *) (** 64-bit integer register-register instructions *) | Paddl (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) @@ -769,6 +771,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** Conversions *) | Pcvtl2w d s => Next (nextinstr (rs#d <- (Val.loword rs###s))) m + | Pcvtw2l r => + Next (nextinstr (rs#r <- (Val.longofint rs#r))) m + | Pmvw2l d s => + Next (nextinstr (rs#d <- (Val.longofint rs#s))) m (** Unconditional jumps. *) | Pj_l l => |