From da7ba2d116ec11fc2071432305db8ad4fdf4c9c0 Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Thu, 7 Jul 2016 09:35:25 +0200 Subject: Remove unnecessary module paths --- common/Separation.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/common/Separation.v b/common/Separation.v index 27065d1f..a8de7390 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -502,6 +502,26 @@ Proof. - auto. Qed. +Lemma range_contains': + forall chunk b ofs, + (align_chunk chunk | ofs) -> + massert_imp (range b ofs (ofs + size_chunk chunk)) + (contains chunk b ofs (fun v => True)). +Proof. + intros. constructor. + intros. destruct H0 as (D & E & F). + assert (Mem.valid_access m chunk b ofs Freeable). + { split; auto. red; auto. } + split. +- generalize (Memdata.size_chunk_pos chunk). + unfold Ptrofs.max_unsigned. omega. +- split; [assumption|]. + destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. + eauto with mem. + exists v; auto. +- auto. +Qed. + Lemma contains_imp: forall (spec1 spec2: val -> Prop) chunk b ofs, (forall v, spec1 v -> spec2 v) -> -- cgit