functor (M : Memory.Model->
  sig
    module V :
      sig
        type elt = Lang.F.var
        type t = Lang.F.Vars.t
        val empty : t
        val is_empty : t -> bool
        val mem : elt -> t -> bool
        val find : elt -> t -> elt
        val add : elt -> t -> t
        val singleton : elt -> t
        val remove : elt -> t -> t
        val union : t -> t -> t
        val inter : t -> t -> t
        val diff : t -> t -> t
        val compare : t -> t -> int
        val equal : t -> t -> bool
        val subset : t -> t -> bool
        val iter : (elt -> unit) -> t -> unit
        val fold : (elt -> '-> 'a) -> t -> '-> 'a
        val for_all : (elt -> bool) -> t -> bool
        val exists : (elt -> bool) -> t -> bool
        val filter : (elt -> bool) -> t -> t
        val partition : (elt -> bool) -> t -> t * t
        val cardinal : t -> int
        val elements : t -> elt list
        val map : (elt -> elt) -> t -> t
        val mapf : (elt -> elt option) -> t -> t
        val intersect : t -> t -> bool
      end
    module P :
      sig
        type t = WpPropId.prop_id
        val ty : t Type.t
        val name : string
        val descr : t Descr.t
        val packed_descr : Structural_descr.pack
        val reprs : t list
        val equal : t -> t -> bool
        val compare : t -> t -> int
        val hash : t -> int
        val pretty_code : Format.formatter -> t -> unit
        val internal_pretty_code :
          Type.precedence -> Format.formatter -> t -> unit
        val pretty : Format.formatter -> t -> unit
        val varname : t -> string
        val mem_project : (Project_skeleton.t -> bool) -> t -> bool
        val copy : t -> t
      end
    module C :
      sig
        type loc = M.loc
        type value = loc Memory.value
        type sigma = M.Sigma.t
        val cval : value -> Lang.F.term
        val cloc : value -> loc
        val cast : Cil_types.typ -> Cil_types.typ -> value -> value
        val equal_typ : Cil_types.typ -> value -> value -> Lang.F.pred
        val equal_obj : Ctypes.c_object -> value -> value -> Lang.F.pred
        val exp : sigma -> Cil_types.exp -> value
        val cond : sigma -> Cil_types.exp -> Lang.F.pred
        val lval : sigma -> Cil_types.lval -> loc
        val call : sigma -> Cil_types.exp -> loc
        val loc_of_exp : sigma -> Cil_types.exp -> loc
        val val_of_exp : sigma -> Cil_types.exp -> Lang.F.term
        val return : sigma -> Cil_types.typ -> Cil_types.exp -> Lang.F.term
        val is_zero : sigma -> Ctypes.c_object -> loc -> Lang.F.pred
        val is_zero_range :
          sigma ->
          loc -> Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred
        val instance_of : loc -> Cil_types.kernel_function -> Lang.F.pred
      end
    module L :
      sig
        type loc = M.loc
        type sigma = M.Sigma.t
        type value = M.loc Memory.value
        type logic = M.loc Memory.logic
        type region = M.loc Memory.sloc list
        val pp_logic : Format.formatter -> logic -> unit
        val pp_sloc : Format.formatter -> loc Memory.sloc -> unit
        val pp_region : Format.formatter -> region -> unit
        type frame = LogicSemantics.Make(M).frame
        val pp_frame : Format.formatter -> frame -> unit
        val get_frame : unit -> frame
        val in_frame : frame -> ('-> 'b) -> '-> 'b
        val mem_frame : Clabels.c_label -> sigma
        val mem_at_frame : frame -> Clabels.c_label -> sigma
        val frame : Cil_types.kernel_function -> frame
        val frame_copy : frame -> frame
        val call_pre :
          Cil_types.kernel_function -> value list -> sigma -> frame
        val call_post :
          Cil_types.kernel_function ->
          value list -> sigma Memory.sequence -> frame
        val return : unit -> Cil_types.typ
        val result : unit -> Lang.F.var
        val status : unit -> Lang.F.var
        val guards : frame -> Lang.F.pred list
        type env = LogicSemantics.Make(M).env
        val new_env : Cil_types.logic_var list -> env
        val move : env -> sigma -> env
        val sigma : env -> sigma
        val mem_at : env -> Clabels.c_label -> sigma
        val call : sigma -> env
        val term : env -> Cil_types.term -> Lang.F.term
        val pred :
          positive:bool ->
          env -> Cil_types.predicate Cil_types.named -> Lang.F.pred
        val region : env -> Cil_types.term -> region
        val assigns :
          env ->
          Cil_types.identified_term Cil_types.assigns ->
          (Ctypes.c_object * region) list option
        val assigns_from :
          env ->
          Cil_types.identified_term Cil_types.from list ->
          (Ctypes.c_object * region) list
        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 valid :
          sigma -> Memory.acs -> Ctypes.c_object -> region -> Lang.F.pred
        val included :
          Ctypes.c_object ->
          region -> Ctypes.c_object -> region -> Lang.F.pred
        val separated : (Ctypes.c_object * region) list -> Lang.F.pred
      end
    module A :
      sig
        type region = (Ctypes.c_object * M.loc Memory.sloc list) list
        val vars : region -> Lang.F.Vars.t
        val domain : region -> M.Heap.set
        val assigned : M.sigma Memory.sequence -> region -> Lang.F.pred list
      end
    type target =
        Gprop of CfgWP.VC.P.t
      | Geffect of CfgWP.VC.P.t * Cil_datatype.Stmt.t *
          WpPropId.effect_source
      | Gposteffect of CfgWP.VC.P.t
    module TARGET :
      sig
        type t = CfgWP.VC.target
        val hsrc : WpPropId.effect_source -> int
        val hash : CfgWP.VC.target -> int
        val compare : CfgWP.VC.target -> CfgWP.VC.target -> int
        val equal : CfgWP.VC.target -> CfgWP.VC.target -> bool
        val prop_id : CfgWP.VC.target -> CfgWP.VC.P.t
        val source :
          CfgWP.VC.target ->
          (Cil_datatype.Stmt.t * WpPropId.effect_source) option
        val pretty : Format.formatter -> CfgWP.VC.target -> unit
      end
    type effect = {
      e_pid : CfgWP.VC.P.t;
      e_kind : WpPropId.a_kind;
      e_label : Clabels.c_label;
      e_valid : CfgWP.VC.L.sigma;
      e_region : CfgWP.VC.A.region;
      e_warn : Warning.Set.t;
    }
    module EFFECT :
      sig
        type t = CfgWP.VC.effect
        val compare : CfgWP.VC.effect -> CfgWP.VC.effect -> int
      end
    module G :
      sig
        type t = TARGET.t
        type set = Qed.Collection.Make(TARGET).set
        type 'a map = 'Qed.Collection.Make(TARGET).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 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 mem : elt -> t -> bool
            val iter : (elt -> unit) -> t -> unit
            val fold : (elt -> '-> 'a) -> t -> '-> 'a
            val filter : (elt -> bool) -> t -> t
            val partition : (elt -> bool) -> t -> t * t
            val for_all : (elt -> bool) -> t -> bool
            val exists : (elt -> bool) -> t -> bool
            val iter_sorted : (elt -> unit) -> t -> unit
            val fold_sorted : (elt -> '-> 'a) -> t -> '-> 'a
            val union : t -> t -> t
            val inter : t -> t -> t
            val subset : t -> t -> bool
            val intersect : t -> t -> bool
            type 'a mapping = 'a map
            val mapping : (elt -> 'a) -> t -> 'a mapping
          end
      end
    module W :
      sig
        type elt = Warning.t
        type t = Warning.Set.t
        val empty : t
        val is_empty : t -> bool
        val mem : elt -> t -> bool
        val add : elt -> t -> t
        val singleton : elt -> t
        val remove : elt -> t -> t
        val union : t -> t -> t
        val inter : t -> t -> t
        val diff : t -> t -> t
        val compare : t -> t -> int
        val equal : t -> t -> bool
        val subset : t -> t -> bool
        val iter : (elt -> unit) -> t -> unit
        val fold : (elt -> '-> 'a) -> t -> '-> 'a
        val for_all : (elt -> bool) -> t -> bool
        val exists : (elt -> bool) -> t -> bool
        val filter : (elt -> bool) -> t -> t
        val partition : (elt -> bool) -> t -> t * t
        val cardinal : t -> int
        val elements : t -> elt list
        val choose : t -> elt
        val split : elt -> t -> t * bool * t
        val find : elt -> t -> elt
        val of_list : elt list -> t
        val min_elt : t -> elt
        val max_elt : t -> elt
        val nearest_elt_le : elt -> t -> elt
        val nearest_elt_ge : elt -> t -> elt
      end
    module D :
      sig
        type elt = Property.t
        type t = Property.Set.t
        val empty : t
        val is_empty : t -> bool
        val mem : elt -> t -> bool
        val add : elt -> t -> t
        val singleton : elt -> t
        val remove : elt -> t -> t
        val union : t -> t -> t
        val inter : t -> t -> t
        val diff : t -> t -> t
        val subset : t -> t -> bool
        val iter : (elt -> unit) -> t -> unit
        val fold : (elt -> '-> 'a) -> t -> '-> 'a
        val for_all : (elt -> bool) -> t -> bool
        val exists : (elt -> bool) -> t -> bool
        val filter : (elt -> bool) -> t -> t
        val partition : (elt -> bool) -> t -> t * t
        val cardinal : t -> int
        val elements : t -> elt list
        val choose : t -> elt
        val split : elt -> t -> t * bool * t
        val find : elt -> t -> elt
        val of_list : elt list -> t
        val min_elt : t -> elt
        val max_elt : t -> elt
        val nearest_elt_le : elt -> t -> elt
        val nearest_elt_ge : elt -> t -> elt
        val ty : t Type.t
        val name : string
        val descr : t Descr.t
        val packed_descr : Structural_descr.pack
        val reprs : t list
        val equal : t -> t -> bool
        val compare : t -> t -> int
        val hash : t -> int
        val pretty_code : Format.formatter -> t -> unit
        val internal_pretty_code :
          Type.precedence -> Format.formatter -> t -> unit
        val pretty : Format.formatter -> t -> unit
        val varname : t -> string
        val mem_project : (Project_skeleton.t -> bool) -> t -> bool
        val copy : t -> t
      end
    module S :
      sig
        type elt = Cil_datatype.Stmt.t
        type t = Cil_datatype.Stmt.Set.t
        val empty : t
        val is_empty : t -> bool
        val mem : elt -> t -> bool
        val add : elt -> t -> t
        val singleton : elt -> t
        val remove : elt -> t -> t
        val union : t -> t -> t
        val inter : t -> t -> t
        val diff : t -> t -> t
        val subset : t -> t -> bool
        val iter : (elt -> unit) -> t -> unit
        val fold : (elt -> '-> 'a) -> t -> '-> 'a
        val for_all : (elt -> bool) -> t -> bool
        val exists : (elt -> bool) -> t -> bool
        val filter : (elt -> bool) -> t -> t
        val partition : (elt -> bool) -> t -> t * t
        val cardinal : t -> int
        val elements : t -> elt list
        val choose : t -> elt
        val split : elt -> t -> t * bool * t
        val find : elt -> t -> elt
        val of_list : elt list -> t
        val min_elt : t -> elt
        val max_elt : t -> elt
        val nearest_elt_le : elt -> t -> elt
        val nearest_elt_ge : elt -> t -> elt
        val ty : t Type.t
        val name : string
        val descr : t Descr.t
        val packed_descr : Structural_descr.pack
        val reprs : t list
        val equal : t -> t -> bool
        val compare : t -> t -> int
        val hash : t -> int
        val pretty_code : Format.formatter -> t -> unit
        val internal_pretty_code :
          Type.precedence -> Format.formatter -> t -> unit
        val pretty : Format.formatter -> t -> unit
        val varname : t -> string
        val mem_project : (Project_skeleton.t -> bool) -> t -> bool
        val copy : t -> t
      end
    module Eset :
      sig
        type elt = EFFECT.t
        type t = FCSet.Make(EFFECT).t
        val empty : t
        val is_empty : t -> bool
        val mem : elt -> t -> bool
        val add : elt -> t -> t
        val singleton : elt -> t
        val remove : elt -> t -> t
        val union : t -> t -> t
        val inter : t -> t -> t
        val diff : t -> t -> t
        val compare : t -> t -> int
        val equal : t -> t -> bool
        val subset : t -> t -> bool
        val iter : (elt -> unit) -> t -> unit
        val fold : (elt -> '-> 'a) -> t -> '-> 'a
        val for_all : (elt -> bool) -> t -> bool
        val exists : (elt -> bool) -> t -> bool
        val filter : (elt -> bool) -> t -> t
        val partition : (elt -> bool) -> t -> t * t
        val cardinal : t -> int
        val elements : t -> elt list
        val choose : t -> elt
        val split : elt -> t -> t * bool * t
        val find : elt -> t -> elt
        val of_list : elt list -> t
        val min_elt : t -> elt
        val max_elt : t -> elt
        val nearest_elt_le : elt -> t -> elt
        val nearest_elt_ge : elt -> t -> elt
      end
    module Gset :
      sig
        type elt = G.t
        type t = G.set
        val empty : t
        val add : elt -> t -> t
        val singleton : elt -> t
        val elements : t -> elt list
        val mem : elt -> t -> bool
        val iter : (elt -> unit) -> t -> unit
        val fold : (elt -> '-> 'a) -> t -> '-> 'a
        val filter : (elt -> bool) -> t -> t
        val partition : (elt -> bool) -> t -> t * t
        val for_all : (elt -> bool) -> t -> bool
        val exists : (elt -> bool) -> t -> bool
        val iter_sorted : (elt -> unit) -> t -> unit
        val fold_sorted : (elt -> '-> 'a) -> t -> '-> 'a
        val union : t -> t -> t
        val inter : t -> t -> t
        val subset : t -> t -> bool
        val intersect : t -> t -> bool
        type 'a mapping = 'G.map
        val mapping : (elt -> 'a) -> t -> 'a mapping
      end
    module Gmap :
      sig
        type key = G.t
        type 'a t = 'G.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 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 = G.set
        val domain : 'a t -> domain
      end
    type vc = {
      hyps : Conditions.bundle;
      goal : Lang.F.pred;
      vars : Lang.F.Vars.t;
      warn : CfgWP.VC.W.t;
      deps : CfgWP.VC.D.t;
      path : CfgWP.VC.S.t;
    }
    type t_env = { frame : CfgWP.VC.L.frame; main : CfgWP.VC.L.env; }
    type t_prop = {
      sigma : CfgWP.VC.L.sigma option;
      effects : CfgWP.VC.Eset.t;
      vcs : CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t;
    }
    val pp_vc : Format.formatter -> CfgWP.VC.vc -> unit
    val pp_vcs : Format.formatter -> CfgWP.VC.vc Splitter.t -> unit
    val pp_gvcs :
      Format.formatter -> CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t -> unit
    val pretty : Format.formatter -> CfgWP.VC.t_prop -> unit
    val empty_vc : CfgWP.VC.vc
    val sigma_opt : M.Sigma.t option -> M.Sigma.t
    val sigma_at : CfgWP.VC.t_prop -> CfgWP.VC.L.sigma
    val sigma_any : call:bool -> CfgWP.VC.t_prop -> M.Sigma.t
    val sigma_union :
      M.Sigma.t option ->
      M.Sigma.t option -> M.Sigma.t * Passive.t * Passive.t
    val merge_sigma :
      M.Sigma.t option ->
      M.Sigma.t option -> M.Sigma.t option * Passive.t * Passive.t
    val join_with : M.Sigma.t -> M.Sigma.t option -> Passive.t
    val occurs_vc : CfgWP.VC.vc -> Lang.F.Vars.elt -> bool
    val intersect_vc : CfgWP.VC.vc -> Lang.F.pred -> bool
    val assume_vc :
      descr:string ->
      ?hpid:WpPropId.prop_id ->
      ?stmt:CfgWP.VC.S.elt ->
      ?warn:Warning.Set.t -> Lang.F.pred list -> CfgWP.VC.vc -> CfgWP.VC.vc
    val passify_vc : Passive.t -> CfgWP.VC.vc -> CfgWP.VC.vc
    val branch_vc :
      stmt:Cil_types.stmt ->
      Lang.F.pred -> CfgWP.VC.vc -> CfgWP.VC.vc -> CfgWP.VC.vc
    val merge_vc : CfgWP.VC.vc -> CfgWP.VC.vc -> CfgWP.VC.vc
    val merge_vcs : CfgWP.VC.vc list -> CfgWP.VC.vc
    val gmerge :
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val gmap :
      ('-> 'b) ->
      'Splitter.t CfgWP.VC.Gmap.t -> 'Splitter.t CfgWP.VC.Gmap.t
    val gbranch :
      left:('-> 'b) ->
      both:('-> '-> 'b) ->
      right:('-> 'b) ->
      'Splitter.t CfgWP.VC.Gmap.t ->
      'Splitter.t CfgWP.VC.Gmap.t -> 'Splitter.t CfgWP.VC.Gmap.t
    val merge_all_vcs :
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t list ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val empty : CfgWP.VC.t_prop
    val merge :
      CfgWP.VC.t_env -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val new_env :
      ?lvars:Cil_types.logic_var list ->
      Cil_types.kernel_function -> CfgWP.VC.t_env
    val in_wenv :
      CfgWP.VC.t_env ->
      CfgWP.VC.t_prop -> (CfgWP.VC.L.env -> CfgWP.VC.t_prop -> 'a) -> 'a
    val intros :
      Lang.F.pred list -> Lang.F.pred -> Lang.F.pred list * Lang.F.pred
    val introduction :
      Lang.F.pred -> Lang.F.Vars.t * Lang.F.pred list * Lang.F.pred
    val add_vc :
      CfgWP.VC.Gmap.key ->
      ?warn:CfgWP.VC.W.t ->
      Lang.F.pred ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val cc_effect :
      CfgWP.VC.L.env ->
      CfgWP.VC.P.t -> WpPropId.assigns_desc -> CfgWP.VC.effect option
    val cc_posteffect :
      CfgWP.VC.effect ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val add_axiom : '-> '-> unit
    val add_hyp :
      CfgWP.VC.t_env ->
      WpPropId.prop_id * Cil_types.predicate Cil_types.named ->
      CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val add_goal :
      CfgWP.VC.t_env ->
      CfgWP.VC.P.t * Cil_types.predicate Cil_types.named ->
      CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val add_assigns :
      CfgWP.VC.t_env ->
      CfgWP.VC.P.t * WpPropId.assigns_desc ->
      CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val add_warnings :
      CfgWP.VC.W.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val assigns_condition :
      CfgWP.VC.A.region -> CfgWP.VC.effect -> Lang.F.pred
    exception COLLECTED
    val is_collected : 'Splitter.t CfgWP.VC.Gmap.t -> CfgWP.VC.P.t -> bool
    val check_nothing :
      CfgWP.VC.Eset.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val check_assigns :
      Cil_datatype.Stmt.t option ->
      WpPropId.effect_source ->
      ?warn:Warning.Set.t ->
      CfgWP.VC.A.region ->
      CfgWP.VC.Eset.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val do_assigns :
      descr:string ->
      ?stmt:Cil_datatype.Stmt.t ->
      source:WpPropId.effect_source ->
      ?hpid:WpPropId.prop_id ->
      ?warn:Warning.Set.t ->
      M.sigma Memory.sequence ->
      CfgWP.VC.A.region ->
      CfgWP.VC.Eset.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val do_assigns_everything :
      ?stmt:Cil_datatype.Stmt.t ->
      ?warn:CfgWP.VC.W.t ->
      CfgWP.VC.Eset.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val cc_assigned :
      CfgWP.VC.L.env ->
      WpPropId.a_kind ->
      Cil_types.identified_term Cil_types.from list ->
      CfgWP.VC.L.sigma Memory.sequence *
      (Ctypes.c_object * CfgWP.VC.L.region) list
    val use_assigns :
      CfgWP.VC.t_env ->
      Cil_datatype.Stmt.t option ->
      WpPropId.prop_id option ->
      WpPropId.assigns_desc -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val is_stopeffect : Clabels.c_label -> CfgWP.VC.effect -> bool
    val not_posteffect : CfgWP.VC.Eset.t -> CfgWP.VC.target -> '-> bool
    val label :
      CfgWP.VC.t_env -> Clabels.c_label -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val cc_lval :
      CfgWP.VC.L.env ->
      Cil_types.lval ->
      Ctypes.c_object * M.Heap.set * CfgWP.VC.L.sigma Memory.sequence *
      CfgWP.VC.C.loc
    val cc_stored :
      M.sigma Memory.sequence ->
      M.loc -> Ctypes.c_object -> Cil_types.exp -> Lang.F.pred list
    val assign :
      CfgWP.VC.t_env ->
      Cil_datatype.Stmt.t ->
      Cil_types.lval -> Cil_types.exp -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val return :
      CfgWP.VC.t_env ->
      CfgWP.VC.S.elt ->
      Cil_types.exp option -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val condition :
      descr:string ->
      ?stmt:CfgWP.VC.S.elt ->
      ?warn:Warning.Set.t ->
      Passive.t -> Lang.F.pred list -> CfgWP.VC.vc -> CfgWP.VC.vc
    val mark :
      Splitter.tag -> CfgWP.VC.vc Splitter.t option -> CfgWP.VC.vc Splitter.t
    val random : unit -> Lang.F.pred
    val pp_opt :
      (Format.formatter -> '-> unit) ->
      Format.formatter -> 'a option -> unit
    val test :
      CfgWP.VC.t_env ->
      CfgWP.VC.S.elt ->
      Cil_types.exp -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val cc_case_values :
      int64 list ->
      Lang.F.term list ->
      CfgWP.VC.C.sigma -> Cil_types.exp list -> int64 list * Lang.F.term list
    val cc_group_case :
      CfgWP.VC.S.elt ->
      Warning.Set.t ->
      string ->
      Splitter.tag ->
      Passive.t ->
      Lang.F.pred list ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val cc_case :
      CfgWP.VC.S.elt ->
      Warning.Set.t ->
      CfgWP.VC.C.sigma ->
      Lang.F.term ->
      Cil_types.exp list * CfgWP.VC.t_prop ->
      Lang.F.term list * CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val cc_default :
      CfgWP.VC.S.elt ->
      M.Sigma.t ->
      Lang.F.pred list ->
      CfgWP.VC.t_prop -> CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val switch :
      CfgWP.VC.t_env ->
      CfgWP.VC.S.elt ->
      Cil_types.exp ->
      (Cil_types.exp list * CfgWP.VC.t_prop) list ->
      CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val init_value :
      CfgWP.VC.t_env ->
      Cil_types.lval ->
      Cil_types.typ ->
      Cil_types.exp option -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val init_range :
      CfgWP.VC.t_env ->
      Cil_types.lval ->
      Cil_types.typ -> int64 -> int64 -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val loop_step : '-> 'a
    val loop_entry : '-> 'a
    val call_instances :
      CfgWP.VC.C.sigma ->
      CfgWP.VC.P.t ->
      Cil_types.exp ->
      Cil_types.kernel_function list ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val call_contract :
      CfgWP.VC.S.elt ->
      M.Sigma.t ->
      (Warning.Set.t * CfgWP.VC.C.loc) option ->
      Kernel_function.t * CfgWP.VC.t_prop ->
      CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
    val call_dynamic :
      CfgWP.VC.t_env ->
      CfgWP.VC.S.elt ->
      CfgWP.VC.P.t ->
      Cil_types.exp ->
      (Kernel_function.t * CfgWP.VC.t_prop) list -> CfgWP.VC.t_prop
    val call_goal_precond :
      CfgWP.VC.t_env ->
      '->
      Cil_types.kernel_function ->
      Cil_types.exp list ->
      pre:(CfgWP.VC.P.t * Cil_types.predicate Cil_types.named) list ->
      CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    type callenv = {
      sigma_pre : M.sigma;
      seq_post : M.sigma Memory.sequence;
      seq_exit : M.sigma Memory.sequence;
      seq_result : M.sigma Memory.sequence;
      loc_result : (Cil_types.typ * Ctypes.c_object * M.loc) option;
      frame_pre : CfgWP.VC.L.frame;
      frame_post : CfgWP.VC.L.frame;
      frame_exit : CfgWP.VC.L.frame;
    }
    val cc_result_domain : Cil_types.lval option -> M.Heap.Set.t option
    val cc_call_domain :
      CfgWP.VC.L.env ->
      Cil_types.kernel_function ->
      Cil_types.exp list ->
      Cil_types.identified_term Cil_types.assigns -> M.Heap.set option
    val cc_havoc :
      M.Sigma.domain option -> M.Sigma.t -> M.Sigma.t Memory.sequence
    val cc_callenv :
      CfgWP.VC.L.env ->
      Cil_types.lval option ->
      Cil_types.kernel_function ->
      Cil_types.exp list ->
      Cil_types.identified_term Cil_types.assigns ->
      CfgWP.VC.t_prop -> CfgWP.VC.t_prop -> CfgWP.VC.callenv
    type call_vcs = {
      vcs_post : CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t;
      vcs_exit : CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t;
    }
    val cc_call_effects :
      Cil_datatype.Stmt.t ->
      CfgWP.VC.callenv ->
      CfgWP.VC.L.env ->
      Cil_types.identified_term Cil_types.assigns ->
      CfgWP.VC.t_prop -> CfgWP.VC.t_prop -> CfgWP.VC.call_vcs
    val cc_contract_hyp :
      CfgWP.VC.L.frame ->
      CfgWP.VC.L.env ->
      ('a * Cil_types.predicate Cil_types.named) list -> Lang.F.pred list
    val cc_result : CfgWP.VC.callenv -> Lang.F.pred list
    val cc_status : CfgWP.VC.L.frame -> CfgWP.VC.L.frame -> Lang.F.pred
    val call_proper :
      CfgWP.VC.t_env ->
      Cil_datatype.Stmt.t ->
      Cil_types.lval option ->
      Kernel_function.t ->
      Cil_types.exp list ->
      pre:('a * Cil_types.predicate Cil_types.named) list ->
      post:('b * Cil_types.predicate Cil_types.named) list ->
      pexit:('c * Cil_types.predicate Cil_types.named) list ->
      assigns:Cil_types.identified_term Cil_types.assigns ->
      p_post:CfgWP.VC.t_prop ->
      p_exit:CfgWP.VC.t_prop -> unit -> CfgWP.VC.t_prop
    val call :
      CfgWP.VC.t_env ->
      Cil_datatype.Stmt.t ->
      Cil_types.lval option ->
      Kernel_function.t ->
      Cil_types.exp list ->
      pre:('a * Cil_types.predicate Cil_types.named) list ->
      post:('b * Cil_types.predicate Cil_types.named) list ->
      pexit:('c * Cil_types.predicate Cil_types.named) list ->
      assigns:Cil_types.identified_term Cil_types.assigns ->
      p_post:CfgWP.VC.t_prop -> p_exit:CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val scope :
      CfgWP.VC.t_env ->
      Cil_types.varinfo list ->
      Mcfg.scope -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val close : CfgWP.VC.t_env -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val cc_from :
      CfgWP.VC.D.t -> Lang.F.pred list -> CfgWP.VC.vc -> CfgWP.VC.vc
    val build_prop_of_from :
      CfgWP.VC.t_env ->
      (WpPropId.prop_id * Cil_types.predicate Cil_types.named) list ->
      CfgWP.VC.t_prop -> CfgWP.VC.t_prop
    val is_trivial : CfgWP.VC.vc -> bool
    val is_empty : CfgWP.VC.vc -> bool
    val make_vcqs :
      CfgWP.VC.target ->
      Splitter.tag list -> CfgWP.VC.vc -> Wpo.VC_Annot.t Bag.t
    val make_trivial : CfgWP.VC.vc -> Wpo.VC_Annot.t
    val make_oblig :
      Wpo.index -> WpPropId.prop_id -> Emitter.t -> Wpo.VC_Annot.t -> Wpo.t
    module PMAP :
      sig
        type key = P.t
        type 'a t = 'FCMap.Make(P).t
        val empty : 'a t
        val is_empty : 'a t -> bool
        val mem : key -> 'a t -> bool
        val add : key -> '-> 'a t -> 'a t
        val singleton : key -> '-> 'a t
        val remove : key -> 'a t -> 'a t
        val merge :
          (key -> 'a option -> 'b option -> 'c option) ->
          'a t -> 'b t -> 'c t
        val compare : ('-> '-> int) -> 'a t -> 'a t -> int
        val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
        val iter : (key -> '-> unit) -> 'a t -> unit
        val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
        val for_all : (key -> '-> bool) -> 'a t -> bool
        val exists : (key -> '-> bool) -> 'a t -> bool
        val filter : (key -> '-> bool) -> 'a t -> 'a t
        val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t
        val cardinal : 'a t -> int
        val bindings : 'a t -> (key * 'a) list
        val min_binding : 'a t -> key * 'a
        val max_binding : 'a t -> key * 'a
        val choose : 'a t -> key * 'a
        val split : key -> 'a t -> 'a t * 'a option * 'a t
        val find : key -> 'a t -> 'a
        val map : ('-> 'b) -> 'a t -> 'b t
        val mapi : (key -> '-> 'b) -> 'a t -> 'b t
      end
    type group = {
      mutable verifs : Wpo.VC_Annot.t Bag.t;
      mutable trivial : CfgWP.VC.vc;
    }
    val group_vc :
      CfgWP.VC.group CfgWP.VC.PMAP.t Pervasives.ref ->
      CfgWP.VC.target -> Splitter.tag list -> CfgWP.VC.vc -> unit
    val compile :
      Wpo.t Bag.t Pervasives.ref -> Wpo.index -> CfgWP.VC.t_prop -> unit
    val compile_lemma : LogicUsage.logic_lemma -> unit
    val prove_lemma :
      Wpo.t Bag.t Pervasives.ref -> LogicUsage.logic_lemma -> unit
  end