sig
  module Make :
    functor (M : Sigs.Model)
      (L : sig
             module M :
               sig
                 val configure : unit -> WpContext.rollback
                 val configure_ia :
                   Interpreted_automata.automaton ->
                   Interpreted_automata.vertex Sigs.binder
                 val datatype : string
                 val hypotheses :
                   MemoryContext.partition -> MemoryContext.partition
                 module Chunk :
                   sig
                     type t = M.Chunk.t
                     val self : string
                     val hash : t -> int
                     val equal : t -> t -> bool
                     val compare : t -> t -> int
                     val pretty : Format.formatter -> t -> unit
                     val tau_of_chunk : t -> Lang.F.tau
                     val basename_of_chunk : t -> string
                     val is_framed : t -> bool
                   end
                 module Heap :
                   sig
                     type t = Chunk.t
                     type set = M.Heap.set
                     type 'a map = 'M.Heap.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 diff : t -> t -> t
                         val subset : t -> t -> bool
                         val intersect : t -> t -> bool
                         val of_list : elt list -> t
                         type 'a mapping = 'a map
                         val mapping : (elt -> 'a) -> t -> 'a mapping
                       end
                   end
                 module Sigma :
                   sig
                     type chunk = Chunk.t
                     module Chunk :
                       sig
                         type t = Chunk.t
                         type set = Heap.set
                         type 'a map = 'Heap.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 diff : t -> t -> t
                             val subset : t -> t -> bool
                             val intersect : t -> t -> bool
                             val of_list : elt list -> t
                             type 'a mapping = 'a map
                             val mapping : (elt -> 'a) -> t -> 'a mapping
                           end
                       end
                     type domain = Chunk.Set.t
                     type t = M.Sigma.t
                     val pretty : Format.formatter -> t -> unit
                     val create : unit -> t
                     val mem : t -> chunk -> bool
                     val get : t -> chunk -> Lang.F.var
                     val value : t -> chunk -> Lang.F.term
                     val copy : t -> t
                     val join : t -> t -> Passive.t
                     val assigned :
                       pre:t -> post:t -> domain -> Lang.F.pred Bag.t
                     val choose : t -> t -> t
                     val merge : t -> t -> t * Passive.t * Passive.t
                     val merge_list : t list -> t * Passive.t list
                     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_chunk : t -> chunk -> t
                     val havoc : t -> domain -> t
                     val havoc_any : call:bool -> t -> t
                     val remove_chunks : t -> domain -> t
                     val domain : t -> domain
                     val union : domain -> domain -> domain
                     val empty : domain
                     val writes : t Sigs.sequence -> domain
                   end
                 type loc = M.loc
                 type chunk = Chunk.t
                 type sigma = Sigma.t
                 type domain = Sigma.domain
                 type segment = loc Sigs.rloc
                 type state = M.state
                 val state : sigma -> state
                 val lookup : state -> Lang.F.term -> Sigs.mval
                 val updates :
                   state Sigs.sequence -> Lang.F.Vars.t -> Sigs.update Bag.t
                 val apply : (Lang.F.term -> Lang.F.term) -> state -> state
                 val iter :
                   (Sigs.mval -> Lang.F.term -> unit) -> state -> unit
                 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 base_offset : loc -> Lang.F.term
                 val block_length :
                   sigma -> Ctypes.c_object -> loc -> Lang.F.term
                 val cast : Ctypes.c_object Sigs.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 -> domain
                 val is_well_formed : sigma -> Lang.F.pred
                 val load : sigma -> Ctypes.c_object -> loc -> loc Sigs.value
                 val load_init :
                   sigma -> Ctypes.c_object -> loc -> Lang.F.term
                 val copied :
                   sigma Sigs.sequence ->
                   Ctypes.c_object -> loc -> loc -> Sigs.equation list
                 val copied_init :
                   sigma Sigs.sequence ->
                   Ctypes.c_object -> loc -> loc -> Sigs.equation list
                 val stored :
                   sigma Sigs.sequence ->
                   Ctypes.c_object ->
                   loc -> Lang.F.term -> Sigs.equation list
                 val stored_init :
                   sigma Sigs.sequence ->
                   Ctypes.c_object ->
                   loc -> Lang.F.term -> Sigs.equation list
                 val assigned :
                   sigma Sigs.sequence ->
                   Ctypes.c_object -> loc Sigs.sloc -> Sigs.equation 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 -> Sigs.acs -> segment -> Lang.F.pred
                 val frame : sigma -> Lang.F.pred list
                 val alloc : sigma -> Cil_types.varinfo list -> sigma
                 val initialized : sigma -> segment -> Lang.F.pred
                 val invalid : sigma -> segment -> Lang.F.pred
                 val scope :
                   sigma Sigs.sequence ->
                   Sigs.scope -> Cil_types.varinfo list -> 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
             type loc = M.loc
             type nonrec value = M.loc Sigs.value
             type nonrec logic = M.loc Sigs.logic
             type nonrec region = M.loc Sigs.region
             type nonrec result = M.loc Sigs.result
             type sigma = M.Sigma.t
             type frame
             val pp_frame : Format.formatter -> frame -> unit
             val get_frame : unit -> frame
             val in_frame : frame -> ('-> 'b) -> '-> 'b
             val mem_at_frame : frame -> Clabels.c_label -> sigma
             val set_at_frame : frame -> Clabels.c_label -> sigma -> unit
             val has_at_frame : frame -> Clabels.c_label -> bool
             val mem_frame : Clabels.c_label -> sigma
             val mk_frame :
               ?kf:Cil_types.kernel_function ->
               ?result:result ->
               ?status:Lang.F.var ->
               ?formals:value Cil_datatype.Varinfo.Map.t ->
               ?labels:sigma Clabels.LabelMap.t ->
               ?descr:string -> unit -> frame
             val local : descr:string -> frame
             val frame : Cil_types.kernel_function -> frame
             type call
             val call :
               ?result:M.loc ->
               Cil_types.kernel_function -> value list -> call
             val call_pre : sigma -> call -> sigma -> frame
             val call_post : sigma -> call -> sigma Sigs.sequence -> frame
             val return : unit -> Cil_types.typ
             val result : unit -> result
             val status : unit -> Lang.F.var
             val guards : frame -> Lang.F.pred list
             type env
             val mk_env :
               ?here:sigma -> ?lvars:Cil_types.logic_var list -> unit -> env
             val current : env -> sigma
             val move_at : env -> sigma -> env
             val mem_at : env -> Clabels.c_label -> sigma
             val env_at : env -> Clabels.c_label -> env
             val lval : env -> Cil_types.term_lval -> Cil_types.typ * M.loc
             val term : env -> Cil_types.term -> Lang.F.term
             val pred :
               Sigs.polarity -> env -> Cil_types.predicate -> Lang.F.pred
             val region : env -> Cil_types.term -> region
             val assigned_of_lval : env -> Cil_types.lval -> region
             val assigned_of_froms : env -> Cil_types.from list -> region
             val assigned_of_assigns :
               env -> Cil_types.assigns -> region option
             val val_of_term : env -> Cil_types.term -> Lang.F.term
             val loc_of_term : env -> Cil_types.term -> loc
             val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
             val vars : region -> Lang.F.Vars.t
             val occurs : Lang.F.var -> region -> bool
             val check_assigns :
               unfold:int ->
               sigma -> written:region -> assignable:region -> Lang.F.pred
           end)
      ->
      sig
        module M :
          sig
            val configure : unit -> WpContext.rollback
            val configure_ia :
              Interpreted_automata.automaton ->
              Interpreted_automata.vertex Sigs.binder
            val datatype : string
            val hypotheses :
              MemoryContext.partition -> MemoryContext.partition
            module Chunk :
              sig
                type t = M.Chunk.t
                val self : string
                val hash : t -> int
                val equal : t -> t -> bool
                val compare : t -> t -> int
                val pretty : Format.formatter -> t -> unit
                val tau_of_chunk : t -> Lang.F.tau
                val basename_of_chunk : t -> string
                val is_framed : t -> bool
              end
            module Heap :
              sig
                type t = Chunk.t
                type set = M.Heap.set
                type 'a map = 'M.Heap.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 diff : t -> t -> t
                    val subset : t -> t -> bool
                    val intersect : t -> t -> bool
                    val of_list : elt list -> t
                    type 'a mapping = 'a map
                    val mapping : (elt -> 'a) -> t -> 'a mapping
                  end
              end
            module Sigma :
              sig
                type chunk = Chunk.t
                module Chunk :
                  sig
                    type t = Chunk.t
                    type set = Heap.set
                    type 'a map = 'Heap.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 diff : t -> t -> t
                        val subset : t -> t -> bool
                        val intersect : t -> t -> bool
                        val of_list : elt list -> t
                        type 'a mapping = 'a map
                        val mapping : (elt -> 'a) -> t -> 'a mapping
                      end
                  end
                type domain = Chunk.Set.t
                type t = M.Sigma.t
                val pretty : Format.formatter -> t -> unit
                val create : unit -> t
                val mem : t -> chunk -> bool
                val get : t -> chunk -> Lang.F.var
                val value : t -> chunk -> Lang.F.term
                val copy : t -> t
                val join : t -> t -> Passive.t
                val assigned : pre:t -> post:t -> domain -> Lang.F.pred Bag.t
                val choose : t -> t -> t
                val merge : t -> t -> t * Passive.t * Passive.t
                val merge_list : t list -> t * Passive.t list
                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_chunk : t -> chunk -> t
                val havoc : t -> domain -> t
                val havoc_any : call:bool -> t -> t
                val remove_chunks : t -> domain -> t
                val domain : t -> domain
                val union : domain -> domain -> domain
                val empty : domain
                val writes : t Sigs.sequence -> domain
              end
            type loc = M.loc
            type chunk = Chunk.t
            type sigma = Sigma.t
            type domain = Sigma.domain
            type segment = loc Sigs.rloc
            type state = M.state
            val state : sigma -> state
            val lookup : state -> Lang.F.term -> Sigs.mval
            val updates :
              state Sigs.sequence -> Lang.F.Vars.t -> Sigs.update Bag.t
            val apply : (Lang.F.term -> Lang.F.term) -> state -> state
            val iter : (Sigs.mval -> Lang.F.term -> unit) -> state -> unit
            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 base_offset : loc -> Lang.F.term
            val block_length : sigma -> Ctypes.c_object -> loc -> Lang.F.term
            val cast : Ctypes.c_object Sigs.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 -> domain
            val is_well_formed : sigma -> Lang.F.pred
            val load : sigma -> Ctypes.c_object -> loc -> loc Sigs.value
            val load_init : sigma -> Ctypes.c_object -> loc -> Lang.F.term
            val copied :
              sigma Sigs.sequence ->
              Ctypes.c_object -> loc -> loc -> Sigs.equation list
            val copied_init :
              sigma Sigs.sequence ->
              Ctypes.c_object -> loc -> loc -> Sigs.equation list
            val stored :
              sigma Sigs.sequence ->
              Ctypes.c_object -> loc -> Lang.F.term -> Sigs.equation list
            val stored_init :
              sigma Sigs.sequence ->
              Ctypes.c_object -> loc -> Lang.F.term -> Sigs.equation list
            val assigned :
              sigma Sigs.sequence ->
              Ctypes.c_object -> loc Sigs.sloc -> Sigs.equation 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 -> Sigs.acs -> segment -> Lang.F.pred
            val frame : sigma -> Lang.F.pred list
            val alloc : sigma -> Cil_types.varinfo list -> sigma
            val initialized : sigma -> segment -> Lang.F.pred
            val invalid : sigma -> segment -> Lang.F.pred
            val scope :
              sigma Sigs.sequence ->
              Sigs.scope -> Cil_types.varinfo list -> 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
        module L :
          sig
            module M :
              sig
                val configure : unit -> WpContext.rollback
                val configure_ia :
                  Interpreted_automata.automaton ->
                  Interpreted_automata.vertex Sigs.binder
                val datatype : string
                val hypotheses :
                  MemoryContext.partition -> MemoryContext.partition
                module Chunk :
                  sig
                    type t = M.Chunk.t
                    val self : string
                    val hash : t -> int
                    val equal : t -> t -> bool
                    val compare : t -> t -> int
                    val pretty : Format.formatter -> t -> unit
                    val tau_of_chunk : t -> Lang.F.tau
                    val basename_of_chunk : t -> string
                    val is_framed : t -> bool
                  end
                module Heap :
                  sig
                    type t = Chunk.t
                    type set = M.Heap.set
                    type 'a map = 'M.Heap.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 diff : t -> t -> t
                        val subset : t -> t -> bool
                        val intersect : t -> t -> bool
                        val of_list : elt list -> t
                        type 'a mapping = 'a map
                        val mapping : (elt -> 'a) -> t -> 'a mapping
                      end
                  end
                module Sigma :
                  sig
                    type chunk = Chunk.t
                    module Chunk :
                      sig
                        type t = Chunk.t
                        type set = Heap.set
                        type 'a map = 'Heap.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 diff : t -> t -> t
                            val subset : t -> t -> bool
                            val intersect : t -> t -> bool
                            val of_list : elt list -> t
                            type 'a mapping = 'a map
                            val mapping : (elt -> 'a) -> t -> 'a mapping
                          end
                      end
                    type domain = Chunk.Set.t
                    type t = M.Sigma.t
                    val pretty : Format.formatter -> t -> unit
                    val create : unit -> t
                    val mem : t -> chunk -> bool
                    val get : t -> chunk -> Lang.F.var
                    val value : t -> chunk -> Lang.F.term
                    val copy : t -> t
                    val join : t -> t -> Passive.t
                    val assigned :
                      pre:t -> post:t -> domain -> Lang.F.pred Bag.t
                    val choose : t -> t -> t
                    val merge : t -> t -> t * Passive.t * Passive.t
                    val merge_list : t list -> t * Passive.t list
                    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_chunk : t -> chunk -> t
                    val havoc : t -> domain -> t
                    val havoc_any : call:bool -> t -> t
                    val remove_chunks : t -> domain -> t
                    val domain : t -> domain
                    val union : domain -> domain -> domain
                    val empty : domain
                    val writes : t Sigs.sequence -> domain
                  end
                type loc = M.loc
                type chunk = Chunk.t
                type sigma = Sigma.t
                type domain = Sigma.domain
                type segment = loc Sigs.rloc
                type state = M.state
                val state : sigma -> state
                val lookup : state -> Lang.F.term -> Sigs.mval
                val updates :
                  state Sigs.sequence -> Lang.F.Vars.t -> Sigs.update Bag.t
                val apply : (Lang.F.term -> Lang.F.term) -> state -> state
                val iter :
                  (Sigs.mval -> Lang.F.term -> unit) -> state -> unit
                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 base_offset : loc -> Lang.F.term
                val block_length :
                  sigma -> Ctypes.c_object -> loc -> Lang.F.term
                val cast : Ctypes.c_object Sigs.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 -> domain
                val is_well_formed : sigma -> Lang.F.pred
                val load : sigma -> Ctypes.c_object -> loc -> loc Sigs.value
                val load_init :
                  sigma -> Ctypes.c_object -> loc -> Lang.F.term
                val copied :
                  sigma Sigs.sequence ->
                  Ctypes.c_object -> loc -> loc -> Sigs.equation list
                val copied_init :
                  sigma Sigs.sequence ->
                  Ctypes.c_object -> loc -> loc -> Sigs.equation list
                val stored :
                  sigma Sigs.sequence ->
                  Ctypes.c_object -> loc -> Lang.F.term -> Sigs.equation list
                val stored_init :
                  sigma Sigs.sequence ->
                  Ctypes.c_object -> loc -> Lang.F.term -> Sigs.equation list
                val assigned :
                  sigma Sigs.sequence ->
                  Ctypes.c_object -> loc Sigs.sloc -> Sigs.equation 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 -> Sigs.acs -> segment -> Lang.F.pred
                val frame : sigma -> Lang.F.pred list
                val alloc : sigma -> Cil_types.varinfo list -> sigma
                val initialized : sigma -> segment -> Lang.F.pred
                val invalid : sigma -> segment -> Lang.F.pred
                val scope :
                  sigma Sigs.sequence ->
                  Sigs.scope -> Cil_types.varinfo list -> 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
            type loc = M.loc
            type nonrec value = M.loc Sigs.value
            type nonrec logic = M.loc Sigs.logic
            type nonrec region = M.loc Sigs.region
            type nonrec result = M.loc Sigs.result
            type sigma = M.Sigma.t
            type frame = L.frame
            val pp_frame : Format.formatter -> frame -> unit
            val get_frame : unit -> frame
            val in_frame : frame -> ('-> 'b) -> '-> 'b
            val mem_at_frame : frame -> Clabels.c_label -> sigma
            val set_at_frame : frame -> Clabels.c_label -> sigma -> unit
            val has_at_frame : frame -> Clabels.c_label -> bool
            val mem_frame : Clabels.c_label -> sigma
            val mk_frame :
              ?kf:Cil_types.kernel_function ->
              ?result:result ->
              ?status:Lang.F.var ->
              ?formals:value Cil_datatype.Varinfo.Map.t ->
              ?labels:sigma Clabels.LabelMap.t ->
              ?descr:string -> unit -> frame
            val local : descr:string -> frame
            val frame : Cil_types.kernel_function -> frame
            type call = L.call
            val call :
              ?result:M.loc ->
              Cil_types.kernel_function -> value list -> call
            val call_pre : sigma -> call -> sigma -> frame
            val call_post : sigma -> call -> sigma Sigs.sequence -> frame
            val return : unit -> Cil_types.typ
            val result : unit -> result
            val status : unit -> Lang.F.var
            val guards : frame -> Lang.F.pred list
            type env = L.env
            val mk_env :
              ?here:sigma -> ?lvars:Cil_types.logic_var list -> unit -> env
            val current : env -> sigma
            val move_at : env -> sigma -> env
            val mem_at : env -> Clabels.c_label -> sigma
            val env_at : env -> Clabels.c_label -> env
            val lval : env -> Cil_types.term_lval -> Cil_types.typ * M.loc
            val term : env -> Cil_types.term -> Lang.F.term
            val pred :
              Sigs.polarity -> env -> Cil_types.predicate -> Lang.F.pred
            val region : env -> Cil_types.term -> region
            val assigned_of_lval : env -> Cil_types.lval -> region
            val assigned_of_froms : env -> Cil_types.from list -> region
            val assigned_of_assigns :
              env -> Cil_types.assigns -> region option
            val val_of_term : env -> Cil_types.term -> Lang.F.term
            val loc_of_term : env -> Cil_types.term -> loc
            val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
            val vars : region -> Lang.F.Vars.t
            val occurs : Lang.F.var -> region -> bool
            val check_assigns :
              unfold:int ->
              sigma -> written:region -> assignable:region -> Lang.F.pred
          end
        val domain : M.loc Sigs.region -> M.Heap.set
        val apply_assigns :
          M.sigma Sigs.sequence -> M.loc Sigs.region -> Lang.F.pred list
      end
end