diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-23 15:58:21 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:09 +0200 |
| commit | 8d196f0f3193758a6371d9eb539af350202e0f4f (patch) | |
| tree | 3a434028437588a39c0b6220b85e4732f112dbfc /mppa_k1c/Asm.v | |
| parent | c81c303db03ba732bda8612381e8569db181a541 (diff) | |
| download | compcert-kvx-8d196f0f3193758a6371d9eb539af350202e0f4f.tar.gz compcert-kvx-8d196f0f3193758a6371d9eb539af350202e0f4f.zip | |
MPPA - Added Mgoto + Pj_l
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 707273a6..82ec101c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -216,8 +216,8 @@ Inductive instruction : Type := | Pcvtw2l (r: ireg) (**r int32 signed -> int64 (pseudo) *) (* Unconditional jumps. Links are always to X1/RA. *) - | Pj_l (l: label) (**r jump to label *) - | Pj_s (symb: ident) (sg: signature) (**r jump to symbol *) +*)| Pj_l (l: label) (**r jump to label *) +(*| Pj_s (symb: ident) (sg: signature) (**r jump to symbol *) | Pj_r (r: ireg) (sg: signature) (**r jump register *) | Pjal_s (symb: ident) (sg: signature) (**r jump-and-link symbol *) | Pjal_r (r: ireg) (sg: signature) (**r jump-and-link register *) @@ -767,9 +767,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#r <- (Val.longofint rs#r))) m (** Unconditional jumps. Links are always to X1/RA. *) - | Pj_l l => +*)| Pj_l l => goto_label f l rs m - | Pj_s s sg => +(*| Pj_s s sg => Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m | Pj_r r sg => Next (rs#PC <- (rs#r)) m |