diff options
Diffstat (limited to 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 79ef016a..d8b81689 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -149,7 +149,7 @@ Lemma contains_get_stack: Proof. intros. unfold load_stack. replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). - eapply loadv_rule; eauto. + eapply loadv_rule; eauto using perm_F_any. simpl. rewrite Ptrofs.add_zero_l; auto. Qed. @@ -171,7 +171,7 @@ Lemma contains_set_stack: Proof. intros. unfold store_stack. replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). - eapply storev_rule; eauto. + eapply storev_rule; eauto using perm_F_any. simpl. rewrite Ptrofs.add_zero_l; auto. Qed. @@ -1087,14 +1087,14 @@ Local Opaque b fe. apply (frame_env_separated b) in SEP. replace (make_env b) with fe in SEP by auto. (* Store of parent *) rewrite sep_swap3 in SEP. - apply (range_contains Mptr) in SEP; [|tauto]. + apply range_contains in SEP;[|apply perm_F_any|tauto]. exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tptr). rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto. clear SEP; intros (m3' & STORE_PARENT & SEP). rewrite sep_swap3 in SEP. (* Store of return address *) rewrite sep_swap4 in SEP. - apply (range_contains Mptr) in SEP; [|tauto]. + apply range_contains in SEP; [|apply perm_F_any|tauto]. exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tptr). rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto. clear SEP; intros (m4' & STORE_RETADDR & SEP). |