sig   val configure : Model.tuning   val datatype : string   val separation : unit -> Separation.clause list   module Chunk : Memory.Chunk   module Heap :     sig       type t = Chunk.t       type set       type 'a map       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       module Map :         sig           type key = t           type 'a t = 'a map           val empty : 'a t           val add : key -> '-> 'a t -> 'a t           val mem : key -> 'a t -> bool           val find : key -> 'a t -> 'a           val findk : key -> 'a t -> key * 'a           val size : 'a t -> int           val is_empty : 'a t -> bool           val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t           val change :             (key -> '-> 'a option -> 'a option) ->             key -> '-> 'a t -> 'a t           val map : ('-> 'b) -> 'a t -> 'b t           val mapi : (key -> '-> 'b) -> 'a t -> 'b t           val mapf : (key -> '-> 'b option) -> 'a t -> 'b t           val mapq : (key -> '-> 'a option) -> 'a t -> 'a t           val filter : (key -> '-> bool) -> 'a t -> 'a t           val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t           val iter : (key -> '-> unit) -> 'a t -> unit           val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b           val iter_sorted : (key -> '-> unit) -> 'a t -> unit           val fold_sorted : (key -> '-> '-> 'b) -> 'a t -> '-> 'b           val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t           val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t           val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t           val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t           val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t           val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool           val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool           val iterk : (key -> '-> '-> unit) -> 'a t -> 'b t -> unit           val iter2 :             (key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit           val merge :             (key -> 'a option -> 'b option -> 'c option) ->             'a t -> 'b t -> 'c t           type domain = set           val domain : 'a t -> domain         end       module Set :         sig           type elt = t           type t = set           val empty : t           val add : elt -> t -> t           val singleton : elt -> t           val elements : t -> elt list           val is_empty : t -> bool           val mem : elt -> t -> bool           val iter : (elt -> unit) -> t -> unit           val fold : (elt -> '-> 'a) -> t -> '-> 'a           val filter : (elt -> bool) -> t -> t           val partition : (elt -> bool) -> t -> t * t           val for_all : (elt -> bool) -> t -> bool           val exists : (elt -> bool) -> t -> bool           val iter_sorted : (elt -> unit) -> t -> unit           val fold_sorted : (elt -> '-> 'a) -> t -> '-> 'a           val union : t -> t -> t           val inter : t -> t -> t           val subset : t -> t -> bool           val intersect : t -> t -> bool           type 'a mapping = 'a map           val mapping : (elt -> 'a) -> t -> 'a mapping         end     end   module Sigma :     sig       type chunk = Chunk.t       type domain = Heap.set       type t       val create : unit -> t       val copy : t -> t       val merge : t -> t -> t * Passive.t * Passive.t       val join : t -> t -> Passive.t       val assigned : t -> t -> domain -> Lang.F.pred Bag.t       val mem : t -> chunk -> bool       val get : t -> chunk -> Lang.F.var       val value : t -> chunk -> Lang.F.term       val iter : (chunk -> Lang.F.var -> unit) -> t -> unit       val iter2 :         (chunk -> Lang.F.var option -> Lang.F.var option -> unit) ->         t -> t -> unit       val havoc : t -> domain -> t       val havoc_chunk : t -> chunk -> t       val havoc_any : call:bool -> t -> t       val domain : t -> domain       val union : domain -> domain -> domain       val empty : domain       val pretty : Format.formatter -> t -> unit     end   type loc   type chunk = Chunk.t   type sigma = Sigma.t   type segment = loc Memory.rloc   val pretty : Format.formatter -> loc -> unit   val vars : loc -> Lang.F.Vars.t   val occurs : Lang.F.var -> loc -> bool   val null : loc   val literal : eid:int -> Cstring.cst -> loc   val cvar : Cil_types.varinfo -> loc   val pointer_loc : Lang.F.term -> loc   val pointer_val : loc -> Lang.F.term   val field : loc -> Cil_types.fieldinfo -> loc   val shift : loc -> Ctypes.c_object -> Lang.F.term -> loc   val base_addr : loc -> loc   val block_length : sigma -> Ctypes.c_object -> loc -> Lang.F.term   val cast : Ctypes.c_object Memory.sequence -> loc -> loc   val loc_of_int : Ctypes.c_object -> Lang.F.term -> loc   val int_of_loc : Ctypes.c_int -> loc -> Lang.F.term   val domain : Ctypes.c_object -> loc -> Heap.set   val load : sigma -> Ctypes.c_object -> loc -> loc Memory.value   val copied :     sigma Memory.sequence ->     Ctypes.c_object -> loc -> loc -> Lang.F.pred list   val stored :     sigma Memory.sequence ->     Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.pred list   val assigned :     sigma Memory.sequence ->     Ctypes.c_object -> loc Memory.sloc -> Lang.F.pred list   val is_null : loc -> Lang.F.pred   val loc_eq : loc -> loc -> Lang.F.pred   val loc_lt : loc -> loc -> Lang.F.pred   val loc_neq : loc -> loc -> Lang.F.pred   val loc_leq : loc -> loc -> Lang.F.pred   val loc_diff : Ctypes.c_object -> loc -> loc -> Lang.F.term   val valid : sigma -> Memory.acs -> segment -> Lang.F.pred   val scope :     sigma -> Mcfg.scope -> Cil_types.varinfo list -> sigma * Lang.F.pred list   val global : sigma -> Lang.F.term -> Lang.F.pred   val included : segment -> segment -> Lang.F.pred   val separated : segment -> segment -> Lang.F.pred end