sig
  module V = Lang.F.Vars
  module P = WpPropId.PropId
  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 :
        sigma -> Cil_types.kernel_function -> value list -> sigma -> frame
      val call_post :
        sigma ->
        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 is_empty : 'a t -> bool
          val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
          val change :
            (key -> '-> 'a option -> 'a option) ->
            key -> '-> 'a t -> 'a t
          val map : ('-> 'b) -> 'a t -> 'b t
          val mapi : (key -> '-> 'b) -> 'a t -> 'b t
          val mapf : (key -> '-> 'b option) -> 'a t -> 'b t
          val mapq : (key -> '-> 'a option) -> 'a t -> 'a t
          val filter : (key -> '-> bool) -> 'a t -> 'a t
          val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
          val iter_sorted : (key -> '-> unit) -> 'a t -> unit
          val fold_sorted : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
          val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t
          val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t
          val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
          val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
          val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
          val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
          val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
          val iterk : (key -> '-> '-> unit) -> 'a t -> 'b t -> unit
          val iter2 :
            (key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          type domain = set
          val domain : 'a t -> domain
        end
      module Set :
        sig
          type elt = t
          type t = set
          val empty : t
          val add : elt -> t -> t
          val singleton : elt -> t
          val elements : t -> elt list
          val is_empty : t -> bool
          val mem : elt -> t -> bool
          val iter : (elt -> unit) -> t -> unit
          val fold : (elt -> '-> 'a) -> t -> '-> 'a
          val filter : (elt -> bool) -> t -> t
          val partition : (elt -> bool) -> t -> t * t
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val iter_sorted : (elt -> unit) -> t -> unit
          val fold_sorted : (elt -> '-> 'a) -> t -> '-> 'a
          val union : t -> t -> t
          val inter : t -> t -> t
          val subset : t -> t -> bool
          val intersect : t -> t -> bool
          type 'a mapping = 'a map
          val mapping : (elt -> 'a) -> t -> 'a mapping
        end
    end
  module W = Warning.Set
  module D = Property.Set
  module S = Cil_datatype.Stmt.Set
  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 = G.Set
  module Gmap = G.Map
  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_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 -> ?filter:bool -> 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 has_init : t_env -> bool
  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 init_const : t_env -> Cil_types.varinfo -> 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 = WpPropId.PropId.t
      type 'a t = 'FCMap.Make(WpPropId.PropId).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