diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-15 16:01:30 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-15 16:01:30 +0200 |
commit | 72378d9371bc5da342266bcf14231ab568e0f919 (patch) | |
tree | 5bb4762c27165b5fa088a19e7666bf159b48480e | |
parent | 6d4ec0d398dcc9ec766c3f55ba4edbae63fb6a2f (diff) | |
download | compcert-kvx-72378d9371bc5da342266bcf14231ab568e0f919.tar.gz compcert-kvx-72378d9371bc5da342266bcf14231ab568e0f919.zip |
Few minor other changes in proof
-rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 834e11e1..bd2dc985 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1621,12 +1621,12 @@ Proof. exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto. intros (rs' & U' & V'). exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs' m2'). - rewrite chunk_of_Tptr in P. + { rewrite chunk_of_Tptr in P. assert (rs' GPRA = rs0 RA). { apply V'. } assert (rs' SP = rs2 SP). { apply V'; discriminate. } rewrite H4. rewrite H3. rewrite ATLR. - change (rs2 SP) with sp. eexact P. + change (rs2 SP) with sp. eexact P. } intros (rs3 & U & V). assert (EXEC_PROLOGUE: exists rs3', exec_straight_blocks tge tf @@ -1652,7 +1652,7 @@ Proof. } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3'). exploit exec_straight_steps_2; eauto using functions_transl. simpl fn_blocks. simpl fn_blocks in g. omega. constructor. - intros (ofs' & X & Y). + intros (ofs' & X & Y). left; exists (State rs3' m3'); split. eapply exec_straight_steps_1; eauto. simpl fn_blocks. simpl fn_blocks in g. omega. |