val loc_all_regions_from (preserve_liveness: bool) (r: HS.rid) : GTot loc
let loc_all_regions_from
  (preserve_liveness: bool)
  (r: HS.rid)
: GTot loc
= loc_regions preserve_liveness (HS.mod_set (Set.singleton r))
val loc_all_regions_from (preserve_liveness: bool) (r: HS.rid) : GTot loc
let loc_all_regions_from (preserve_liveness: bool) (r: HS.rid) : GTot loc =
loc_regions preserve_liveness (HS.mod_set (Set.singleton r))
FStar.Modifies.fsti.checked
prims.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.ModifiesGen.fsti.checked FStar.Map.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Classical.fsti.checked FStar.Buffer.fst.checked
FStar.Modifies.fsti
Prims.bool FStar.Monotonic.HyperHeap.rid FStar.Modifies.loc_regions FStar.Monotonic.HyperHeap.mod_set FStar.Set.singleton FStar.Modifies.loc
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Modifies

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module B = FStar.Buffer

(*** The modifies clause *)

val loc : Type u#1

val loc_none: loc

val loc_union
  (s1 s2: loc)
: GTot loc

(** The following is useful to make Z3 cut matching loops with
modifies_trans and modifies_refl *)
val loc_union_idem
  (s: loc)
: Lemma
  (loc_union s s == s)
  [SMTPat (loc_union s s)]

val loc_union_comm
  (s1 s2: loc)
: Lemma
  (loc_union s1 s2 == loc_union s2 s1)
  [SMTPat (loc_union s1 s2)]

val loc_union_assoc
  (s1 s2 s3: loc)
: Lemma
  (loc_union s1 (loc_union s2 s3) == loc_union (loc_union s1 s2) s3)

val loc_union_loc_none_l
  (s: loc)
: Lemma
  (loc_union loc_none s == s)
  [SMTPat (loc_union loc_none s)]

val loc_union_loc_none_r
  (s: loc)
: Lemma
  (loc_union s loc_none == s)
  [SMTPat (loc_union s loc_none)]

val loc_buffer
  (#t: Type)
  (b: B.buffer t)
: GTot loc

val loc_addresses
  (preserve_liveness: bool)
  (r: HS.rid)
  (n: Set.set nat)
: GTot loc

val loc_regions
  (preserve_liveness: bool)
  (r: Set.set HS.rid)
: GTot loc

let loc_mreference
  (#a: Type)
  (#p: Preorder.preorder a)
  (b: HS.mreference a p)
: GTot loc
= loc_addresses true (HS.frameOf b) (Set.singleton (HS.as_addr b))

let loc_freed_mreference
  (#a: Type)
  (#p: Preorder.preorder a)
  (b: HS.mreference a p)
: GTot loc
= loc_addresses false (HS.frameOf b) (Set.singleton (HS.as_addr b))

let loc_region_only
  (preserve_liveness: bool)
  (r: HS.rid)
: GTot loc
= loc_regions preserve_liveness (Set.singleton r)

let loc_all_regions_from
  (preserve_liveness: bool)
  (r: HS.rid)
val loc_all_regions_from (preserve_liveness: bool) (r: HS.rid) : GTot loc
preserve_liveness: Prims.bool -> r: FStar.Monotonic.HyperHeap.rid -> Prims.GTot FStar.Modifies.loc