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 copied :
                                    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 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 ->
                                unfold:bool -> Cil_types.term -> region
                              val assigned_of_lval :
                                env ->
                                unfold:bool -> Cil_types.lval -> region
                              val assigned_of_froms :
                                env ->
                                unfold:bool -> Cil_types.from list -> region
                              val assigned_of_assigns :
                                env ->
                                unfold:bool ->
                                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 :
                                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 copied :
              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 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 copied :
                  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 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 -> unfold:bool -> Cil_types.term -> region
            val assigned_of_lval :
              env -> unfold:bool -> Cil_types.lval -> region
            val assigned_of_froms :
              env -> unfold:bool -> Cil_types.from list -> region
            val assigned_of_assigns :
              env -> unfold:bool -> 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 :
              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