diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-06-27 09:26:05 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-06-27 09:26:05 +0200 |
commit | e005f76f8260fbc3c7d60e4142a55bb5e56cf9b0 (patch) | |
tree | 6c188ffdefae96eacab73e93816a239deab2d40c /backend/Unusedglobproof.v | |
parent | c52ce2f847f368391c36166aebe76515b02f7c7c (diff) | |
parent | fb44646eb7308c1dd6a44b85415528982083200b (diff) | |
download | compcert-e005f76f8260fbc3c7d60e4142a55bb5e56cf9b0.tar.gz compcert-e005f76f8260fbc3c7d60e4142a55bb5e56cf9b0.zip |
Merge pull request #102 from AbsInt/memory_permissions
Stricter control of permissions in memory injections and extensions
Diffstat (limited to 'backend/Unusedglobproof.v')
-rw-r--r-- | backend/Unusedglobproof.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index bb40a2d3..44cf1e8a 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -1178,6 +1178,17 @@ Proof. destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. split. omega. generalize (Int.unsigned_range_2 ofs). omega. +- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). + exploit (Genv.init_mem_characterization_gen p); eauto. + exploit (Genv.init_mem_characterization_gen tp); eauto. + destruct gd as [f|v]. ++ intros (P2 & Q2) (P1 & Q1). + apply Q2 in H0. destruct H0. subst. replace ofs with 0 by omega. + left; apply Mem.perm_cur; auto. ++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). + apply Q2 in H0. destruct H0. subst. + left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. + apply P1. omega. Qed. End INIT_MEM. |