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