diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-05 17:25:36 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-05 17:25:36 +0200 |
| commit | 76af54d8ae77f843b7f6f15f9a0fc6124df47ebb (patch) | |
| tree | 8375bead74972832b8fab6ce9e5d30fcde7357b1 /mppa_k1c/Asmblockgenproof.v | |
| parent | 9d94664fa180d909c43992a4cbdf6808fb9c4289 (diff) | |
| download | compcert-kvx-76af54d8ae77f843b7f6f15f9a0fc6124df47ebb.tar.gz compcert-kvx-76af54d8ae77f843b7f6f15f9a0fc6124df47ebb.zip | |
#91 Removed completely the duplicated semantics in Asmblock
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index a071a9f8..1fbe7832 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -259,7 +259,7 @@ Proof. exploit label_pos_code_tail; eauto. instantiate (1 := 0).
intros [pos' [P [Q R]]].
exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).
- split. unfold goto_label. rewrite P. rewrite H1. auto.
+ split. unfold goto_label. unfold par_goto_label. rewrite P. rewrite H1. auto.
split. rewrite Pregmap.gss. constructor; auto.
rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
auto. omega.
@@ -1680,7 +1680,7 @@ Proof. { change (fn_blocks tf) with tfbody; unfold tfbody.
apply exec_straight_blocks_step with rs2 m2'.
unfold exec_bblock. simpl exec_body. rewrite C. fold sp. simpl exec_control.
- rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. reflexivity.
+ rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. rewrite regset_same_assign. reflexivity.
reflexivity.
eapply exec_straight_blocks_trans.
- eexact W'.
|