diff options
| author | Timothy Bourke <tim@tbrk.org> | 2016-07-07 09:35:25 +0200 |
|---|---|---|
| committer | Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr> | 2020-04-21 01:08:58 +0200 |
| commit | da7ba2d116ec11fc2071432305db8ad4fdf4c9c0 (patch) | |
| tree | 4e489d1bace8caf11cc14a5342748da652e32919 | |
| parent | 3358c5ebecf24aec90df610b0cd46585d6af70ca (diff) | |
| download | compcert-kvx-da7ba2d116ec11fc2071432305db8ad4fdf4c9c0.tar.gz compcert-kvx-da7ba2d116ec11fc2071432305db8ad4fdf4c9c0.zip | |
Remove unnecessary module paths
| -rw-r--r-- | common/Separation.v | 20 |
1 files changed, 20 insertions, 0 deletions
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) -> |