diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-09 09:52:04 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-09 09:52:04 +0000 |
| commit | 8a64451e6f474d20a469b939a938577bbe6d3d66 (patch) | |
| tree | e49a52973b9fbf726ba2ceff3e7af0ee2b84e617 /common/Memtype.v | |
| parent | 8a26cc219f8c8211301f021bd0ee4a27153528f8 (diff) | |
| download | compcert-kvx-8a64451e6f474d20a469b939a938577bbe6d3d66.tar.gz compcert-kvx-8a64451e6f474d20a469b939a938577bbe6d3d66.zip | |
Merge of Andrew Tolmach's HASP-related changes
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Memtype.v')
| -rw-r--r-- | common/Memtype.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/common/Memtype.v b/common/Memtype.v index f7635816..2e44331f 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -1159,6 +1159,16 @@ Axiom free_inject: exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) -> inject f m1' m2'. +Axiom drop_outside_inject: + forall f m1 m2 b lo hi p m2', + inject f m1 m2 -> + drop_perm m2 b lo hi p = Some m2' -> + (forall b' delta, + f b' = Some(b, delta) -> + high_bound m1 b' + delta <= lo + \/ hi <= low_bound m1 b' + delta) -> + inject f m1 m2'. + (** Memory states that inject into themselves. *) Definition flat_inj (thr: block) : meminj := |