diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-18 16:13:22 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-18 16:13:22 +0100 |
| commit | aa400a9eed939578917810d32ef4fcf79944729d (patch) | |
| tree | 73015b7cf217f2ed172829ee9a68084ff26d4b16 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 4d25fa871e9960d6e01dd4b63acdf367fee5431b (diff) | |
| download | compcert-kvx-aa400a9eed939578917810d32ef4fcf79944729d.tar.gz compcert-kvx-aa400a9eed939578917810d32ef4fcf79944729d.zip | |
The parent frame pointer is now R17 instead of R14
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2de49faa..33912203 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -67,8 +67,8 @@ Proof. erewrite exec_basic_instr_pc; eauto. Qed. -Lemma next_eq {A: Type}: - forall (rs rs':A) m m', +Lemma next_eq: + forall (rs rs': regset) m m', rs = rs' -> m = m' -> Next rs m = Next rs' m'. Proof. intros. congruence. @@ -136,7 +136,7 @@ Proof. inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite (regset_double_set GPR32 PC); try discriminate. rewrite (regset_double_set GPR12 PC); try discriminate. - rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity. + rewrite (regset_double_set FP PC); try discriminate. reflexivity. - repeat (rewrite Pregmap.gso; try discriminate). destruct (Mem.loadv _ _ _); try discriminate. destruct (rs GPR12); try discriminate. |