functor (M : Memory.Model->
  sig
    module VCG :
      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 =
          VC(M).target =
            Gprop of P.t
          | Geffect of P.t * Cil_datatype.Stmt.t * WpPropId.effect_source
          | Gposteffect of P.t
        module TARGET :
          sig
            type t = target
            val hsrc : WpPropId.effect_source -> int
            val hash : target -> int
            val compare : target -> target -> int
            val equal : target -> target -> bool
            val prop_id : target -> P.t
            val source :
              target -> (Cil_datatype.Stmt.t * WpPropId.effect_source) option
            val pretty : Format.formatter -> target -> unit
          end
        type effect =
          VC(M).effect = {
          e_pid : P.t;
          e_kind : WpPropId.a_kind;
          e_label : Clabels.c_label;
          e_valid : L.sigma;
          e_region : A.region;
          e_warn : Warning.Set.t;
        }
        module EFFECT :
          sig type t = effect val compare : effect -> 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 =
          VC(M).vc = {
          hyps : Conditions.bundle;
          goal : Lang.F.pred;
          vars : Lang.F.Vars.t;
          warn : W.t;
          deps : D.t;
          path : S.t;
        }
        type t_env = VC(M).t_env = { frame : L.frame; main : L.env; }
        type t_prop =
          VC(M).t_prop = {
          sigma : L.sigma option;
          effects : Eset.t;
          vcs : vc Splitter.t Gmap.t;
        }
        val pp_vc : Format.formatter -> vc -> unit
        val pp_vcs : Format.formatter -> vc Splitter.t -> unit
        val pp_gvcs : Format.formatter -> vc Splitter.t Gmap.t -> unit
        val pretty : Format.formatter -> t_prop -> unit
        val empty_vc : vc
        val sigma_opt : M.Sigma.t option -> M.Sigma.t
        val sigma_at : t_prop -> L.sigma
        val sigma_any : call:bool -> 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 : vc -> Lang.F.Vars.elt -> bool
        val intersect_vc : vc -> Lang.F.pred -> bool
        val assume_vc :
          descr:string ->
          ?hpid:WpPropId.prop_id ->
          ?stmt:S.elt -> ?warn:Warning.Set.t -> Lang.F.pred list -> vc -> vc
        val passify_vc : Passive.t -> vc -> vc
        val branch_vc : stmt:Cil_types.stmt -> Lang.F.pred -> vc -> vc -> vc
        val merge_vc : vc -> vc -> vc
        val merge_vcs : vc list -> vc
        val gmerge :
          vc Splitter.t Gmap.t ->
          vc Splitter.t Gmap.t -> vc Splitter.t Gmap.t
        val gmap : ('-> 'b) -> 'Splitter.t Gmap.t -> 'Splitter.t Gmap.t
        val gbranch :
          left:('-> 'b) ->
          both:('-> '-> 'b) ->
          right:('-> 'b) ->
          'Splitter.t Gmap.t ->
          'Splitter.t Gmap.t -> 'Splitter.t Gmap.t
        val merge_all_vcs : vc Splitter.t Gmap.t list -> vc Splitter.t Gmap.t
        val empty : t_prop
        val merge : t_env -> t_prop -> t_prop -> t_prop
        val new_env :
          ?lvars:Cil_types.logic_var list ->
          Cil_types.kernel_function -> t_env
        val in_wenv : t_env -> t_prop -> (L.env -> 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 :
          Gmap.key ->
          ?warn:W.t ->
          Lang.F.pred -> vc Splitter.t Gmap.t -> vc Splitter.t Gmap.t
        val cc_effect :
          L.env -> P.t -> WpPropId.assigns_desc -> effect option
        val cc_posteffect :
          effect -> vc Splitter.t Gmap.t -> vc Splitter.t Gmap.t
        val add_axiom : '-> '-> unit
        val add_hyp :
          t_env ->
          WpPropId.prop_id * Cil_types.predicate Cil_types.named ->
          t_prop -> t_prop
        val add_goal :
          t_env ->
          P.t * Cil_types.predicate Cil_types.named -> t_prop -> t_prop
        val add_assigns :
          t_env -> P.t * WpPropId.assigns_desc -> t_prop -> t_prop
        val add_warnings :
          W.t -> vc Splitter.t Gmap.t -> vc Splitter.t Gmap.t
        val assigns_condition : A.region -> effect -> Lang.F.pred
        exception COLLECTED
        val is_collected : 'Splitter.t Gmap.t -> P.t -> bool
        val check_nothing :
          Eset.t -> vc Splitter.t Gmap.t -> vc Splitter.t Gmap.t
        val check_assigns :
          Cil_datatype.Stmt.t option ->
          WpPropId.effect_source ->
          ?warn:Warning.Set.t ->
          A.region -> Eset.t -> vc Splitter.t Gmap.t -> vc Splitter.t 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 ->
          A.region -> Eset.t -> vc Splitter.t Gmap.t -> vc Splitter.t Gmap.t
        val do_assigns_everything :
          ?stmt:Cil_datatype.Stmt.t ->
          ?warn:W.t -> Eset.t -> vc Splitter.t Gmap.t -> vc Splitter.t Gmap.t
        val cc_assigned :
          L.env ->
          WpPropId.a_kind ->
          Cil_types.identified_term Cil_types.from list ->
          L.sigma Memory.sequence * (Ctypes.c_object * L.region) list
        val use_assigns :
          t_env ->
          Cil_datatype.Stmt.t option ->
          WpPropId.prop_id option ->
          WpPropId.assigns_desc -> t_prop -> t_prop
        val is_stopeffect : Clabels.c_label -> effect -> bool
        val not_posteffect : Eset.t -> target -> '-> bool
        val label : t_env -> Clabels.c_label -> t_prop -> t_prop
        val cc_lval :
          L.env ->
          Cil_types.lval ->
          Ctypes.c_object * M.Heap.set * L.sigma Memory.sequence * C.loc
        val cc_stored :
          M.sigma Memory.sequence ->
          M.loc -> Ctypes.c_object -> Cil_types.exp -> Lang.F.pred list
        val assign :
          t_env ->
          Cil_datatype.Stmt.t ->
          Cil_types.lval -> Cil_types.exp -> t_prop -> t_prop
        val return :
          t_env -> S.elt -> Cil_types.exp option -> t_prop -> t_prop
        val condition :
          descr:string ->
          ?stmt:S.elt ->
          ?warn:Warning.Set.t -> Passive.t -> Lang.F.pred list -> vc -> vc
        val mark : Splitter.tag -> vc Splitter.t option -> vc Splitter.t
        val random : unit -> Lang.F.pred
        val pp_opt :
          (Format.formatter -> '-> unit) ->
          Format.formatter -> 'a option -> unit
        val test :
          t_env -> S.elt -> Cil_types.exp -> t_prop -> t_prop -> t_prop
        val cc_case_values :
          int64 list ->
          Lang.F.term list ->
          C.sigma -> Cil_types.exp list -> int64 list * Lang.F.term list
        val cc_group_case :
          S.elt ->
          Warning.Set.t ->
          string ->
          Splitter.tag ->
          Passive.t ->
          Lang.F.pred list -> vc Splitter.t Gmap.t -> vc Splitter.t Gmap.t
        val cc_case :
          S.elt ->
          Warning.Set.t ->
          C.sigma ->
          Lang.F.term ->
          Cil_types.exp list * t_prop ->
          Lang.F.term list * vc Splitter.t Gmap.t
        val cc_default :
          S.elt ->
          M.Sigma.t -> Lang.F.pred list -> t_prop -> vc Splitter.t Gmap.t
        val switch :
          t_env ->
          S.elt ->
          Cil_types.exp ->
          (Cil_types.exp list * t_prop) list -> t_prop -> t_prop
        val init_value :
          t_env ->
          Cil_types.lval ->
          Cil_types.typ -> Cil_types.exp option -> t_prop -> t_prop
        val init_range :
          t_env ->
          Cil_types.lval ->
          Cil_types.typ -> int64 -> int64 -> t_prop -> t_prop
        val loop_step : '-> 'a
        val loop_entry : '-> 'a
        val call_instances :
          C.sigma ->
          P.t ->
          Cil_types.exp ->
          Cil_types.kernel_function list ->
          vc Splitter.t Gmap.t -> vc Splitter.t Gmap.t
        val call_contract :
          S.elt ->
          M.Sigma.t ->
          (Warning.Set.t * C.loc) option ->
          Kernel_function.t * t_prop -> vc Splitter.t Gmap.t
        val call_dynamic :
          t_env ->
          S.elt ->
          P.t -> Cil_types.exp -> (Kernel_function.t * t_prop) list -> t_prop
        val call_goal_precond :
          t_env ->
          '->
          Cil_types.kernel_function ->
          Cil_types.exp list ->
          pre:(P.t * Cil_types.predicate Cil_types.named) list ->
          t_prop -> t_prop
        type callenv =
          VC(M).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 : L.frame;
          frame_post : L.frame;
          frame_exit : L.frame;
        }
        val cc_result_domain : Cil_types.lval option -> M.Heap.Set.t option
        val cc_call_domain :
          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 :
          L.env ->
          Cil_types.lval option ->
          Cil_types.kernel_function ->
          Cil_types.exp list ->
          Cil_types.identified_term Cil_types.assigns ->
          t_prop -> t_prop -> callenv
        type call_vcs =
          VC(M).call_vcs = {
          vcs_post : vc Splitter.t Gmap.t;
          vcs_exit : vc Splitter.t Gmap.t;
        }
        val cc_call_effects :
          Cil_datatype.Stmt.t ->
          callenv ->
          L.env ->
          Cil_types.identified_term Cil_types.assigns ->
          t_prop -> t_prop -> call_vcs
        val cc_contract_hyp :
          L.frame ->
          L.env ->
          ('a * Cil_types.predicate Cil_types.named) list -> Lang.F.pred list
        val cc_result : callenv -> Lang.F.pred list
        val cc_status : L.frame -> L.frame -> Lang.F.pred
        val call_proper :
          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:t_prop -> p_exit:t_prop -> unit -> t_prop
        val call :
          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:t_prop -> p_exit:t_prop -> t_prop
        val scope :
          t_env -> Cil_types.varinfo list -> Mcfg.scope -> t_prop -> t_prop
        val close : t_env -> t_prop -> t_prop
        val cc_from : D.t -> Lang.F.pred list -> vc -> vc
        val build_prop_of_from :
          t_env ->
          (WpPropId.prop_id * Cil_types.predicate Cil_types.named) list ->
          t_prop -> t_prop
        val is_trivial : vc -> bool
        val is_empty : vc -> bool
        val make_vcqs :
          target -> Splitter.tag list -> vc -> Wpo.VC_Annot.t Bag.t
        val make_trivial : 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 =
          VC(M).group = {
          mutable verifs : Wpo.VC_Annot.t Bag.t;
          mutable trivial : vc;
        }
        val group_vc :
          group PMAP.t ref -> target -> Splitter.tag list -> vc -> unit
        val compile : Wpo.t Bag.t ref -> Wpo.index -> t_prop -> unit
        val compile_lemma : LogicUsage.logic_lemma -> unit
        val prove_lemma : Wpo.t Bag.t ref -> LogicUsage.logic_lemma -> unit
      end
    module WP :
      sig
        val compute :
          Cil2cfg.t ->
          WpStrategy.strategy ->
          VCG.t_prop list * (Format.formatter -> Cil2cfg.edge -> unit)
      end
    class thecomputer :
      Model.t ->
      object
        val mutable annots : WpStrategy.strategy Bag.t
        val mutable lemmas : LogicUsage.logic_lemma Bag.t
        method add_lemma : LogicUsage.logic_lemma -> unit
        method add_strategy : WpStrategy.strategy -> unit
        method compute : Wpo.t Bag.t
        method lemma : bool
      end
    val create : Model.t -> Generator.computer
  end