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/Asmblockdeps.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/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c5b5bd56..b77fa47d 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -750,7 +750,7 @@ Proof. rewrite H. rewrite MEMAL. rewrite MEMS. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. - destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]; subst; Simpl. + destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl. (* Freeframe *) - simpl in H. destruct (Mem.loadv _ _ _) eqn:MLOAD; try discriminate. destruct (rs GPR12) eqn:SPeq; try discriminate. destruct (Mem.free _ _ _ _) eqn:MFREE; try discriminate. inv H. inv H0. @@ -758,7 +758,7 @@ Proof. * simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite SPeq. rewrite MLOAD. rewrite MFREE. Simpl. rewrite e. rewrite SPeq. rewrite MLOAD. rewrite MFREE. reflexivity. * Simpl. - * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]; subst; Simpl. + * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl. (* Pget *) - simpl in H. destruct rs0 eqn:rs0eq; try discriminate. inv H. inv H0. eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. |