sig   type 'a sequence = { pre : 'a; post : 'a; }   type acs = RW | RD   type 'a value = Val of Wp.Lang.F.term | Loc of 'a   type 'a rloc =       Rloc of Wp.Ctypes.c_object * 'a     | Rrange of 'a * Wp.Ctypes.c_object * Wp.Lang.F.term option *         Wp.Lang.F.term option   type 'a sloc =       Sloc of 'a     | Sarray of 'a * Wp.Ctypes.c_object * int     | Srange of 'a * Wp.Ctypes.c_object * Wp.Lang.F.term option *         Wp.Lang.F.term option     | Sdescr of Wp.Lang.F.var list * 'a * Wp.Lang.F.pred   type 'a logic =       Vexp of Wp.Lang.F.term     | Vloc of 'a     | Vset of Wp.Vset.set     | Lset of 'Wp.Memory.sloc list   module type Chunk =     sig       type t       val self : string       val hash : Wp.Memory.Chunk.t -> int       val compare : Wp.Memory.Chunk.t -> Wp.Memory.Chunk.t -> int       val pretty : Format.formatter -> Wp.Memory.Chunk.t -> unit       val tau_of_chunk : Wp.Memory.Chunk.t -> Wp.Lang.F.tau       val basename_of_chunk : Wp.Memory.Chunk.t -> string       val is_framed : Wp.Memory.Chunk.t -> bool     end   module type Sigma =     sig       type chunk       type domain       type t       val create : unit -> Wp.Memory.Sigma.t       val copy : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t       val merge :         Wp.Memory.Sigma.t ->         Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t * Wp.Passive.t * Wp.Passive.t       val join : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t -> Wp.Passive.t       val assigned :         Wp.Memory.Sigma.t ->         Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain -> Wp.Lang.F.pred Bag.t       val mem : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> bool       val get : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Lang.F.var       val value :         Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Lang.F.term       val iter :         (Wp.Memory.Sigma.chunk -> Wp.Lang.F.var -> unit) ->         Wp.Memory.Sigma.t -> unit       val iter2 :         (Wp.Memory.Sigma.chunk ->          Wp.Lang.F.var option -> Wp.Lang.F.var option -> unit) ->         Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t -> unit       val havoc :         Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain -> Wp.Memory.Sigma.t       val havoc_chunk :         Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Memory.Sigma.t       val havoc_any : call:bool -> Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t       val domain : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain       val union :         Wp.Memory.Sigma.domain ->         Wp.Memory.Sigma.domain -> Wp.Memory.Sigma.domain       val empty : Wp.Memory.Sigma.domain       val pretty : Format.formatter -> Wp.Memory.Sigma.t -> unit     end   module type Model =     sig       val configure : Wp.Model.tuning       val datatype : string       val separation : unit -> Wp.Separation.clause list       module Chunk : 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 = Wp.Memory.Chunk.t       type sigma = Wp.Memory.Model.Sigma.t       type segment = Wp.Memory.Model.loc Wp.Memory.rloc       val pretty : Format.formatter -> Wp.Memory.Model.loc -> unit       val vars : Wp.Memory.Model.loc -> Wp.Lang.F.Vars.t       val occurs : Wp.Lang.F.var -> Wp.Memory.Model.loc -> bool       val null : Wp.Memory.Model.loc       val literal : eid:int -> Wp.Cstring.cst -> Wp.Memory.Model.loc       val cvar : Cil_types.varinfo -> Wp.Memory.Model.loc       val pointer_loc : Wp.Lang.F.term -> Wp.Memory.Model.loc       val pointer_val : Wp.Memory.Model.loc -> Wp.Lang.F.term       val field :         Wp.Memory.Model.loc -> Cil_types.fieldinfo -> Wp.Memory.Model.loc       val shift :         Wp.Memory.Model.loc ->         Wp.Ctypes.c_object -> Wp.Lang.F.term -> Wp.Memory.Model.loc       val base_addr : Wp.Memory.Model.loc -> Wp.Memory.Model.loc       val block_length :         Wp.Memory.Model.sigma ->         Wp.Ctypes.c_object -> Wp.Memory.Model.loc -> Wp.Lang.F.term       val cast :         Wp.Ctypes.c_object Wp.Memory.sequence ->         Wp.Memory.Model.loc -> Wp.Memory.Model.loc       val loc_of_int :         Wp.Ctypes.c_object -> Wp.Lang.F.term -> Wp.Memory.Model.loc       val int_of_loc :         Wp.Ctypes.c_int -> Wp.Memory.Model.loc -> Wp.Lang.F.term       val domain :         Wp.Ctypes.c_object -> Wp.Memory.Model.loc -> Wp.Memory.Model.Heap.set       val load :         Wp.Memory.Model.sigma ->         Wp.Ctypes.c_object ->         Wp.Memory.Model.loc -> Wp.Memory.Model.loc Wp.Memory.value       val copied :         Wp.Memory.Model.sigma Wp.Memory.sequence ->         Wp.Ctypes.c_object ->         Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred list       val stored :         Wp.Memory.Model.sigma Wp.Memory.sequence ->         Wp.Ctypes.c_object ->         Wp.Memory.Model.loc -> Wp.Lang.F.term -> Wp.Lang.F.pred list       val assigned :         Wp.Memory.Model.sigma Wp.Memory.sequence ->         Wp.Ctypes.c_object ->         Wp.Memory.Model.loc Wp.Memory.sloc -> Wp.Lang.F.pred list       val is_null : Wp.Memory.Model.loc -> Wp.Lang.F.pred       val loc_eq :         Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred       val loc_lt :         Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred       val loc_neq :         Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred       val loc_leq :         Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred       val loc_diff :         Wp.Ctypes.c_object ->         Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.term       val valid :         Wp.Memory.Model.sigma ->         Wp.Memory.acs -> Wp.Memory.Model.segment -> Wp.Lang.F.pred       val scope :         Wp.Memory.Model.sigma ->         Wp.Mcfg.scope ->         Cil_types.varinfo list -> Wp.Memory.Model.sigma * Wp.Lang.F.pred list       val global : Wp.Memory.Model.sigma -> Wp.Lang.F.term -> Wp.Lang.F.pred       val included :         Wp.Memory.Model.segment -> Wp.Memory.Model.segment -> Wp.Lang.F.pred       val separated :         Wp.Memory.Model.segment -> Wp.Memory.Model.segment -> Wp.Lang.F.pred     end end