Module MemEmpty

module MemEmpty: sig .. end

module Logic: Qed.Logic
val datatype : string
val configure : unit -> unit
val theories : unit -> 'a list
module Chunk: sig .. end
module Heap: Qed.Collection.Make(Chunk)
module Sigma: Sigma.Make(Chunk)(Heap)
type loc = unit 
type chunk = Chunk.t 
type sigma = Sigma.t 
type segment = loc Memory.rloc 
val pretty : 'a -> unit -> unit
val vars : 'a -> Lang.F.Vars.t
val occurs : 'a -> 'b -> bool
val null : unit
val literal : eid:'a -> 'b -> unit
val cvar : 'a -> unit
val pointer_loc : 'a -> unit
val pointer_val : unit -> Lang.F.term
val field : 'a -> 'b -> unit
val shift : 'a -> 'b -> 'c -> unit
val base_addr : 'a -> unit
val block_length : 'a -> 'b -> 'c -> Lang.F.term
val cast : 'a -> 'b -> unit
val loc_of_int : 'a -> 'b -> unit
val int_of_loc : 'a -> unit -> Lang.F.term
val domain : 'a -> 'b -> Heap.Set.t
val source : string
val load : 'a -> 'b -> unit -> 'c
val copied : 'a -> 'b -> unit -> unit -> 'c list
val stored : 'a -> 'b -> unit -> 'c -> 'd list
val assigned : 'a -> 'b -> 'c -> 'd list
val no_pointer : unit -> 'a
val is_null : 'a -> 'b
val loc_eq : 'a -> 'b -> 'c
val loc_lt : 'a -> 'b -> 'c
val loc_leq : 'a -> 'b -> 'c
val loc_neq : 'a -> 'b -> 'c
val loc_diff : 'a -> 'b -> 'c -> 'd
val valid : 'a -> 'b -> 'c
val scope : 'a -> 'b -> 'c -> 'a * 'd list
val global : 'a -> 'b -> Lang.F.pred
val included : 'a -> 'b -> 'c
val separated : 'a -> 'b -> 'c