diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-13 15:53:31 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:07 +0200 |
| commit | 79597131ae07f1fe63485270486755481549470f (patch) | |
| tree | 6ef89496243889bf4c5eec52f05d18fa08984ff8 /mppa_k1c/Asmgen.v | |
| parent | e3aed59a6d58f4486da40e0a7a381ea0bf10ba81 (diff) | |
| download | compcert-kvx-79597131ae07f1fe63485270486755481549470f.tar.gz compcert-kvx-79597131ae07f1fe63485270486755481549470f.zip | |
MPPA - ABI proof complete (Asmgenproof.v:step_simulation)
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index ba9e6fe8..c8ea4279 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -902,8 +902,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool := match i with | Msetstack src ofs ty => before - | Mgetparam ofs ty dst => negb (mreg_eq dst R30) - | Mop op args res => before && negb (mreg_eq res R30) + | Mgetparam ofs ty dst => negb (mreg_eq dst R32) + | Mop op args res => before && negb (mreg_eq res R32) | _ => false end. |