sig
  module Ctypes :
    sig
      type c_int =
          UInt8
        | SInt8
        | UInt16
        | SInt16
        | UInt32
        | SInt32
        | UInt64
        | SInt64
      val c_int_all : Wp.Ctypes.c_int list
      type c_float = Float32 | Float64
      type arrayflat = {
        arr_size : int;
        arr_dim : int;
        arr_cell : Cil_types.typ;
        arr_cell_nbr : int;
      }
      type arrayinfo = {
        arr_element : Cil_types.typ;
        arr_flat : Wp.Ctypes.arrayflat option;
      }
      type c_object =
          C_int of Wp.Ctypes.c_int
        | C_float of Wp.Ctypes.c_float
        | C_pointer of Cil_types.typ
        | C_comp of Cil_types.compinfo
        | C_array of Wp.Ctypes.arrayinfo
      val object_of_pointed : Wp.Ctypes.c_object -> Wp.Ctypes.c_object
      val object_of_array_elem : Wp.Ctypes.c_object -> Wp.Ctypes.c_object
      val object_of_logic_type : Cil_types.logic_type -> Wp.Ctypes.c_object
      val object_of_logic_pointed :
        Cil_types.logic_type -> Wp.Ctypes.c_object
      val imemo : (Wp.Ctypes.c_int -> 'a) -> Wp.Ctypes.c_int -> 'a
      val fmemo : (Wp.Ctypes.c_float -> 'a) -> Wp.Ctypes.c_float -> 'a
      val is_char : Wp.Ctypes.c_int -> bool
      val c_char : unit -> Wp.Ctypes.c_int
      val c_bool : unit -> Wp.Ctypes.c_int
      val c_ptr : unit -> Wp.Ctypes.c_int
      val c_int : Cil_types.ikind -> Wp.Ctypes.c_int
      val c_float : Cil_types.fkind -> Wp.Ctypes.c_float
      val object_of : Cil_types.typ -> Wp.Ctypes.c_object
      val is_void : Cil_types.typ -> bool
      val is_pointer : Wp.Ctypes.c_object -> bool
      val char : char -> int64
      val constant : Cil_types.exp -> int64
      val get_int : Cil_types.exp -> int64 option
      val i_bits : Wp.Ctypes.c_int -> int
      val i_bytes : Wp.Ctypes.c_int -> int
      val signed : Wp.Ctypes.c_int -> bool
      val c_int_bounds : Wp.Ctypes.c_int -> Integer.t * Integer.t
      val sub_c_int : Wp.Ctypes.c_int -> Wp.Ctypes.c_int -> bool
      val sub_c_float : Wp.Ctypes.c_float -> Wp.Ctypes.c_float -> bool
      val sizeof_defined : Wp.Ctypes.c_object -> bool
      val sizeof_object : Wp.Ctypes.c_object -> int
      val field_offset : Cil_types.fieldinfo -> int
      val no_infinite_array : Wp.Ctypes.c_object -> bool
      val array_dim : Wp.Ctypes.arrayinfo -> Wp.Ctypes.c_object * int
      val array_size : Cil_types.typ -> int option
      val array_dimensions :
        Wp.Ctypes.arrayinfo -> Wp.Ctypes.c_object * int option list
      val dimension_of_object : Wp.Ctypes.c_object -> (int * int) option
      val i_convert : Wp.Ctypes.c_int -> Wp.Ctypes.c_int -> Wp.Ctypes.c_int
      val f_convert :
        Wp.Ctypes.c_float -> Wp.Ctypes.c_float -> Wp.Ctypes.c_float
      val promote :
        Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> Wp.Ctypes.c_object
      val pp_int : Format.formatter -> Wp.Ctypes.c_int -> unit
      val pp_float : Format.formatter -> Wp.Ctypes.c_float -> unit
      val pp_object : Format.formatter -> Wp.Ctypes.c_object -> unit
      val basename : Wp.Ctypes.c_object -> string
      val compare : Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> int
      val equal : Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> bool
      val merge :
        Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> Wp.Ctypes.c_object
      val hash : Wp.Ctypes.c_object -> int
      val pretty : Format.formatter -> Wp.Ctypes.c_object -> unit
      module C_object :
        sig
          type t = c_object
          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 AinfoComparable :
        sig
          type t = Wp.Ctypes.arrayinfo
          val compare :
            Wp.Ctypes.AinfoComparable.t -> Wp.Ctypes.AinfoComparable.t -> int
          val equal :
            Wp.Ctypes.AinfoComparable.t ->
            Wp.Ctypes.AinfoComparable.t -> bool
          val hash : Wp.Ctypes.AinfoComparable.t -> int
        end
      val compare_ptr_conflated :
        Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> int
    end
  module Clabels :
    sig
      type c_label =
          Here
        | Init
        | Pre
        | Post
        | Exit
        | At of string list * int
        | CallAt of int
        | LabelParam of string
      val equal : Wp.Clabels.c_label -> Wp.Clabels.c_label -> bool
      module T :
        sig
          type t = Wp.Clabels.c_label
          val compare : Wp.Clabels.T.t -> Wp.Clabels.T.t -> int
        end
      module LabelMap :
        sig
          type key = c_label
          type +'a 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
      module LabelSet :
        sig
          type elt = c_label
          type 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
      val loop_head_label : Cil_types.stmt -> Cil_types.logic_label
      val mk_logic_label : Cil_types.stmt -> Cil_types.logic_label
      val mk_stmt_label : Cil_types.stmt -> Wp.Clabels.c_label
      val mk_loop_label : Cil_types.stmt -> Wp.Clabels.c_label
      val c_label : Cil_types.logic_label -> Wp.Clabels.c_label
      val pretty : Format.formatter -> Wp.Clabels.c_label -> unit
      val lookup_name : Wp.Clabels.c_label -> string
      val lookup :
        (Cil_types.logic_label * Cil_types.logic_label) list ->
        string -> Wp.Clabels.c_label
    end
  module NormAtLabels :
    sig
      val catch_label_error : exn -> string -> string -> unit
      type label_mapping
      val labels_empty : Wp.NormAtLabels.label_mapping
      val labels_fct_pre : Wp.NormAtLabels.label_mapping
      val labels_fct_post : Wp.NormAtLabels.label_mapping
      val labels_fct_assigns : Wp.NormAtLabels.label_mapping
      val labels_assert_before :
        Cil_types.stmt -> Wp.NormAtLabels.label_mapping
      val labels_assert_after :
        Cil_types.stmt ->
        Cil_types.logic_label option -> Wp.NormAtLabels.label_mapping
      val labels_loop_inv : Cil_types.stmt -> Wp.NormAtLabels.label_mapping
      val labels_loop_assigns :
        Cil_types.stmt -> Wp.NormAtLabels.label_mapping
      val labels_stmt_pre : Cil_types.stmt -> Wp.NormAtLabels.label_mapping
      val labels_stmt_post :
        Cil_types.stmt ->
        Cil_types.logic_label option -> Wp.NormAtLabels.label_mapping
      val labels_stmt_assigns :
        Cil_types.stmt ->
        Cil_types.logic_label option -> Wp.NormAtLabels.label_mapping
      val labels_predicate :
        (Cil_types.logic_label * Cil_types.logic_label) list ->
        Wp.NormAtLabels.label_mapping
      val labels_axiom : Wp.NormAtLabels.label_mapping
      val preproc_annot :
        Wp.NormAtLabels.label_mapping ->
        Cil_types.predicate Cil_types.named ->
        Cil_types.predicate Cil_types.named
      val preproc_assigns :
        Wp.NormAtLabels.label_mapping ->
        Cil_types.identified_term Cil_types.from list ->
        Cil_types.identified_term Cil_types.from list
      val preproc_label :
        Wp.NormAtLabels.label_mapping ->
        Cil_types.logic_label -> Cil_types.logic_label
    end
  module Separation :
    sig
      type region =
          Var of Cil_types.varinfo
        | Ptr of Cil_types.varinfo
        | Arr of Cil_types.varinfo
      val pp_region : Format.formatter -> Wp.Separation.region -> unit
      type clause = {
        mutex : Wp.Separation.region list;
        other : Wp.Separation.region list;
      }
      val is_true : Wp.Separation.clause -> bool
      val requires : Wp.Separation.clause list -> Wp.Separation.clause list
      val pp_clause : Format.formatter -> Wp.Separation.clause -> unit
    end
  module LogicUsage :
    sig
      val basename : Cil_types.varinfo -> string
      type logic_lemma = {
        lem_name : string;
        lem_position : Lexing.position;
        lem_axiom : bool;
        lem_types : string list;
        lem_labels : Cil_types.logic_label list;
        lem_property : Cil_types.predicate Cil_types.named;
        lem_depends : Wp.LogicUsage.logic_lemma list;
      }
      type axiomatic = {
        ax_name : string;
        ax_position : Lexing.position;
        ax_property : Property.t;
        mutable ax_types : Cil_types.logic_type_info list;
        mutable ax_logics : Cil_types.logic_info list;
        mutable ax_lemmas : Wp.LogicUsage.logic_lemma list;
        mutable ax_reads : Cil_datatype.Varinfo.Set.t;
      }
      type logic_section =
          Toplevel of int
        | Axiomatic of Wp.LogicUsage.axiomatic
      val compute : unit -> unit
      val ip_lemma : Wp.LogicUsage.logic_lemma -> Property.t
      val iter_lemmas : (Wp.LogicUsage.logic_lemma -> unit) -> unit
      val logic_lemma : string -> Wp.LogicUsage.logic_lemma
      val axiomatic : string -> Wp.LogicUsage.axiomatic
      val section_of_lemma : string -> Wp.LogicUsage.logic_section
      val section_of_type :
        Cil_types.logic_type_info -> Wp.LogicUsage.logic_section
      val section_of_logic :
        Cil_types.logic_info -> Wp.LogicUsage.logic_section
      val proof_context : unit -> Wp.LogicUsage.logic_lemma list
      val is_recursive : Cil_types.logic_info -> bool
      val get_induction_labels :
        Cil_types.logic_info ->
        string -> Wp.Clabels.LabelSet.t Wp.Clabels.LabelMap.t
      val get_name : Cil_types.logic_info -> string
      val pp_profile : Format.formatter -> Cil_types.logic_info -> unit
      val dump : unit -> unit
    end
  module RefUsage :
    sig
      type access = NoAccess | ByRef | ByArray | ByValue | ByAddr
      val get :
        ?kf:Cil_types.kernel_function ->
        ?init:bool -> Cil_types.varinfo -> Wp.RefUsage.access
      val iter :
        ?kf:Cil_types.kernel_function ->
        ?init:bool ->
        (Cil_types.varinfo -> Wp.RefUsage.access -> unit) -> unit
      val dump : unit -> unit
      val compute : unit -> unit
    end
  module WpPropId :
    sig
      type prop_id
      val property_of_id : Wp.WpPropId.prop_id -> Property.t
      val source_of_id : Wp.WpPropId.prop_id -> Lexing.position
      module PropId :
        sig
          type t = 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
      val compare_prop_id : Wp.WpPropId.prop_id -> Wp.WpPropId.prop_id -> int
      val is_check : Wp.WpPropId.prop_id -> bool
      val is_assigns : Wp.WpPropId.prop_id -> bool
      val is_requires : Property.t -> bool
      val is_loop_preservation : Wp.WpPropId.prop_id -> Cil_types.stmt option
      val select_by_name : string list -> Wp.WpPropId.prop_id -> bool
      val select_call_pre :
        Cil_types.stmt -> Property.t option -> Wp.WpPropId.prop_id -> bool
      val prop_id_keys : Wp.WpPropId.prop_id -> string list * string list
      val get_propid : Wp.WpPropId.prop_id -> string
      val pp_propid : Format.formatter -> Wp.WpPropId.prop_id -> unit
      type prop_kind =
          PKCheck
        | PKProp
        | PKEstablished
        | PKPreserved
        | PKPropLoop
        | PKVarDecr
        | PKVarPos
        | PKAFctOut
        | PKAFctExit
        | PKPre of Cil_types.kernel_function * Cil_types.stmt * Property.t
      val pretty : Format.formatter -> Wp.WpPropId.prop_id -> unit
      val pretty_context :
        Description.kf -> Format.formatter -> Wp.WpPropId.prop_id -> unit
      val pretty_local : Format.formatter -> Wp.WpPropId.prop_id -> unit
      val label_of_prop_id : Wp.WpPropId.prop_id -> string
      val string_of_termination_kind : Cil_types.termination_kind -> string
      val num_of_bhv_from :
        Cil_types.funbehavior ->
        Cil_types.identified_term Cil_types.from -> int
      val mk_code_annot_ids :
        Cil_types.kernel_function ->
        Cil_types.stmt ->
        Cil_types.code_annotation -> Wp.WpPropId.prop_id list
      val mk_assert_id :
        Cil_types.kernel_function ->
        Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
      val mk_establish_id :
        Cil_types.kernel_function ->
        Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
      val mk_preserve_id :
        Cil_types.kernel_function ->
        Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
      val mk_inv_hyp_id :
        Cil_types.kernel_function ->
        Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
      val mk_var_decr_id :
        Cil_types.kernel_function ->
        Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
      val mk_var_pos_id :
        Cil_types.kernel_function ->
        Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
      val mk_loop_from_id :
        Cil_types.kernel_function ->
        Cil_types.stmt ->
        Cil_types.code_annotation ->
        Cil_types.identified_term Cil_types.from -> Wp.WpPropId.prop_id
      val mk_bhv_from_id :
        Cil_types.kernel_function ->
        Cil_types.kinstr ->
        string list ->
        Cil_types.funbehavior ->
        Cil_types.identified_term Cil_types.from -> Wp.WpPropId.prop_id
      val mk_fct_from_id :
        Cil_types.kernel_function ->
        Cil_types.funbehavior ->
        Cil_types.termination_kind ->
        Cil_types.identified_term Cil_types.from -> Wp.WpPropId.prop_id
      val mk_disj_bhv_id :
        Cil_types.kernel_function * Cil_types.kinstr * string list *
        string list -> Wp.WpPropId.prop_id
      val mk_compl_bhv_id :
        Cil_types.kernel_function * Cil_types.kinstr * string list *
        string list -> Wp.WpPropId.prop_id
      val mk_decrease_id :
        Cil_types.kernel_function * Cil_types.kinstr *
        Cil_types.term Cil_types.variant -> Wp.WpPropId.prop_id
      val mk_lemma_id : Wp.LogicUsage.logic_lemma -> Wp.WpPropId.prop_id
      val mk_stmt_assigns_id :
        Cil_types.kernel_function ->
        Cil_types.stmt ->
        string list ->
        Cil_types.funbehavior ->
        Cil_types.identified_term Cil_types.from list ->
        Wp.WpPropId.prop_id option
      val mk_loop_assigns_id :
        Cil_types.kernel_function ->
        Cil_types.stmt ->
        Cil_types.code_annotation ->
        Cil_types.identified_term Cil_types.from list ->
        Wp.WpPropId.prop_id option
      val mk_fct_assigns_id :
        Cil_types.kernel_function ->
        Cil_types.funbehavior ->
        Cil_types.termination_kind ->
        Cil_types.identified_term Cil_types.from list ->
        Wp.WpPropId.prop_id option
      val mk_pre_id :
        Cil_types.kernel_function ->
        Cil_types.kinstr ->
        Cil_types.funbehavior ->
        Cil_types.identified_predicate -> Wp.WpPropId.prop_id
      val mk_stmt_post_id :
        Cil_types.kernel_function ->
        Cil_types.stmt ->
        Cil_types.funbehavior ->
        Cil_types.termination_kind * Cil_types.identified_predicate ->
        Wp.WpPropId.prop_id
      val mk_fct_post_id :
        Cil_types.kernel_function ->
        Cil_types.funbehavior ->
        Cil_types.termination_kind * Cil_types.identified_predicate ->
        Wp.WpPropId.prop_id
      val mk_call_pre_id :
        Cil_types.kernel_function ->
        Cil_types.stmt -> Property.t -> Property.t -> Wp.WpPropId.prop_id
      val mk_property : Property.t -> Wp.WpPropId.prop_id
      val mk_check : Property.t -> Wp.WpPropId.prop_id
      type a_kind = LoopAssigns | StmtAssigns
      type assigns_desc = private {
        a_label : Cil_types.logic_label;
        a_stmt : Cil_types.stmt option;
        a_kind : Wp.WpPropId.a_kind;
        a_assigns : Cil_types.identified_term Cil_types.assigns;
      }
      val pp_assigns_desc :
        Format.formatter -> Wp.WpPropId.assigns_desc -> unit
      type effect_source = FromCode | FromCall | FromReturn
      type assigns_info = Wp.WpPropId.prop_id * Wp.WpPropId.assigns_desc
      val assigns_info_id : Wp.WpPropId.assigns_info -> Wp.WpPropId.prop_id
      type assigns_full_info = private
          AssignsLocations of Wp.WpPropId.assigns_info
        | AssignsAny of Wp.WpPropId.assigns_desc
        | NoAssignsInfo
      val empty_assigns_info : Wp.WpPropId.assigns_full_info
      val mk_assigns_info :
        Wp.WpPropId.prop_id ->
        Wp.WpPropId.assigns_desc -> Wp.WpPropId.assigns_full_info
      val mk_stmt_any_assigns_info :
        Cil_types.stmt -> Wp.WpPropId.assigns_full_info
      val mk_kf_any_assigns_info : unit -> Wp.WpPropId.assigns_full_info
      val mk_loop_any_assigns_info :
        Cil_types.stmt -> Wp.WpPropId.assigns_full_info
      val pp_assign_info :
        string -> Format.formatter -> Wp.WpPropId.assigns_full_info -> unit
      val merge_assign_info :
        Wp.WpPropId.assigns_full_info ->
        Wp.WpPropId.assigns_full_info -> Wp.WpPropId.assigns_full_info
      val mk_loop_assigns_desc :
        Cil_types.stmt ->
        Cil_types.identified_term Cil_types.from list ->
        Wp.WpPropId.assigns_desc
      val mk_stmt_assigns_desc :
        Cil_types.stmt ->
        Cil_types.identified_term Cil_types.from list ->
        Wp.WpPropId.assigns_desc
      val mk_asm_assigns_desc : Cil_types.stmt -> Wp.WpPropId.assigns_desc
      val mk_kf_assigns_desc :
        Cil_types.identified_term Cil_types.from list ->
        Wp.WpPropId.assigns_desc
      val mk_init_assigns : Wp.WpPropId.assigns_desc
      val is_call_assigns : Wp.WpPropId.assigns_desc -> bool
      type axiom_info = Wp.WpPropId.prop_id * Wp.LogicUsage.logic_lemma
      val mk_axiom_info : Wp.LogicUsage.logic_lemma -> Wp.WpPropId.axiom_info
      val pp_axiom_info : Format.formatter -> Wp.WpPropId.axiom_info -> unit
      type pred_info =
          Wp.WpPropId.prop_id * Cil_types.predicate Cil_types.named
      val mk_pred_info :
        Wp.WpPropId.prop_id ->
        Cil_types.predicate Cil_types.named -> Wp.WpPropId.pred_info
      val pred_info_id : Wp.WpPropId.pred_info -> Wp.WpPropId.prop_id
      val pp_pred_of_pred_info :
        Format.formatter -> Wp.WpPropId.pred_info -> unit
      val pp_pred_info : Format.formatter -> Wp.WpPropId.pred_info -> unit
      val mk_part : Wp.WpPropId.prop_id -> int * int -> Wp.WpPropId.prop_id
      val kind_of_id : Wp.WpPropId.prop_id -> Wp.WpPropId.prop_kind
      val parts_of_id : Wp.WpPropId.prop_id -> (int * int) option
      val subproofs : Wp.WpPropId.prop_id -> int
      val subproof_idx : Wp.WpPropId.prop_id -> int
      val get_induction : Wp.WpPropId.prop_id -> Cil_types.stmt option
    end
  module Mcfg :
    sig
      type scope =
          SC_Global
        | SC_Function_in
        | SC_Function_frame
        | SC_Function_out
        | SC_Block_in
        | SC_Block_out
      module type Export =
        sig
          type pred
          type decl
          val export_section : Format.formatter -> string -> unit
          val export_goal :
            Format.formatter -> string -> Wp.Mcfg.Export.pred -> unit
          val export_decl : Format.formatter -> Wp.Mcfg.Export.decl -> unit
        end
      module type Splitter =
        sig
          type pred
          val simplify : Wp.Mcfg.Splitter.pred -> Wp.Mcfg.Splitter.pred
          val split :
            bool -> Wp.Mcfg.Splitter.pred -> Wp.Mcfg.Splitter.pred Bag.t
        end
      module type S =
        sig
          type t_env
          type t_prop
          val pretty : Format.formatter -> Wp.Mcfg.S.t_prop -> unit
          val merge :
            Wp.Mcfg.S.t_env ->
            Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val empty : Wp.Mcfg.S.t_prop
          val new_env :
            ?lvars:Cil_types.logic_var list ->
            Cil_types.kernel_function -> Wp.Mcfg.S.t_env
          val add_axiom :
            Wp.WpPropId.prop_id -> Wp.LogicUsage.logic_lemma -> unit
          val add_hyp :
            Wp.Mcfg.S.t_env ->
            Wp.WpPropId.pred_info -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val add_goal :
            Wp.Mcfg.S.t_env ->
            Wp.WpPropId.pred_info -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val add_assigns :
            Wp.Mcfg.S.t_env ->
            Wp.WpPropId.assigns_info -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val use_assigns :
            Wp.Mcfg.S.t_env ->
            Cil_types.stmt option ->
            Wp.WpPropId.prop_id option ->
            Wp.WpPropId.assigns_desc -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val label :
            Wp.Mcfg.S.t_env ->
            Wp.Clabels.c_label -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val assign :
            Wp.Mcfg.S.t_env ->
            Cil_types.stmt ->
            Cil_types.lval ->
            Cil_types.exp -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val return :
            Wp.Mcfg.S.t_env ->
            Cil_types.stmt ->
            Cil_types.exp option -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val test :
            Wp.Mcfg.S.t_env ->
            Cil_types.stmt ->
            Cil_types.exp ->
            Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val switch :
            Wp.Mcfg.S.t_env ->
            Cil_types.stmt ->
            Cil_types.exp ->
            (Cil_types.exp list * Wp.Mcfg.S.t_prop) list ->
            Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val has_init : Wp.Mcfg.S.t_env -> bool
          val init_value :
            Wp.Mcfg.S.t_env ->
            Cil_types.lval ->
            Cil_types.typ ->
            Cil_types.exp option -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val init_range :
            Wp.Mcfg.S.t_env ->
            Cil_types.lval ->
            Cil_types.typ ->
            Integer.t ->
            Integer.t ->
            Cil_types.exp option -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val init_const :
            Wp.Mcfg.S.t_env ->
            Cil_types.varinfo -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val loop_entry : Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val loop_step : Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val call_dynamic :
            Wp.Mcfg.S.t_env ->
            Cil_types.stmt ->
            Wp.WpPropId.prop_id ->
            Cil_types.exp ->
            (Cil_types.kernel_function * Wp.Mcfg.S.t_prop) list ->
            Wp.Mcfg.S.t_prop
          val call_goal_precond :
            Wp.Mcfg.S.t_env ->
            Cil_types.stmt ->
            Cil_types.kernel_function ->
            Cil_types.exp list ->
            pre:Wp.WpPropId.pred_info list ->
            Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val call :
            Wp.Mcfg.S.t_env ->
            Cil_types.stmt ->
            Cil_types.lval option ->
            Cil_types.kernel_function ->
            Cil_types.exp list ->
            pre:Wp.WpPropId.pred_info list ->
            post:Wp.WpPropId.pred_info list ->
            pexit:Wp.WpPropId.pred_info list ->
            assigns:Cil_types.identified_term Cil_types.assigns ->
            p_post:Wp.Mcfg.S.t_prop ->
            p_exit:Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val scope :
            Wp.Mcfg.S.t_env ->
            Cil_types.varinfo list ->
            Wp.Mcfg.scope -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val close : Wp.Mcfg.S.t_env -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
          val build_prop_of_from :
            Wp.Mcfg.S.t_env ->
            Wp.WpPropId.pred_info list ->
            Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
        end
    end
  module Context :
    sig
      val with_current_loc : Cil_types.location -> ('-> 'b) -> '-> 'b
      type 'a value
      val create : ?default:'-> string -> 'Wp.Context.value
      val defined : 'Wp.Context.value -> bool
      val get : 'Wp.Context.value -> 'a
      val set : 'Wp.Context.value -> '-> unit
      val update : 'Wp.Context.value -> ('-> 'a) -> unit
      val bind : 'Wp.Context.value -> '-> ('-> 'c) -> '-> 'c
      val free : 'Wp.Context.value -> ('-> 'c) -> '-> 'c
      val clear : 'Wp.Context.value -> unit
      val push : 'Wp.Context.value -> '-> 'a option
      val pop : 'Wp.Context.value -> 'a option -> unit
      val name : 'Wp.Context.value -> string
      val once : (unit -> unit) -> unit -> unit
    end
  module Warning :
    sig
      exception Error of string * string
      val error :
        ?source:string ->
        ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
      type t = {
        loc : Lexing.position;
        severe : bool;
        source : string;
        reason : string;
        effect : string;
      }
      val compare : Wp.Warning.t -> Wp.Warning.t -> int
      val pretty : Format.formatter -> Wp.Warning.t -> unit
      module Set :
        sig
          type elt = t
          type 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 Map :
        sig
          type key = t
          type +'a 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
      val severe : Wp.Warning.Set.t -> bool
      type context
      val context : ?source:string -> unit -> Wp.Warning.context
      val flush : Wp.Warning.context -> Wp.Warning.Set.t
      val add : Wp.Warning.t -> unit
      val emit :
        ?severe:bool ->
        ?source:string ->
        effect:string -> ('a, Format.formatter, unit) Pervasives.format -> 'a
      val handle :
        ?severe:bool ->
        effect:string -> handler:('-> 'b) -> ('-> 'b) -> '-> 'b
      type 'a outcome =
          Result of Wp.Warning.Set.t * 'a
        | Failed of Wp.Warning.Set.t
      val catch :
        ?source:string ->
        ?severe:bool ->
        effect:string -> ('-> 'b) -> '-> 'Wp.Warning.outcome
    end
  module Model :
    sig
      module S : Datatype.S_with_collections
      type t = S.t
      type model = S.t
      type tuning = unit -> unit
      type separation = Kernel_function.t -> Wp.Separation.clause list
      val repr : Wp.Model.model
      val register :
        id:string ->
        ?descr:string ->
        ?tuning:Wp.Model.tuning list ->
        ?separation:Wp.Model.separation -> unit -> Wp.Model.model
      val get_id : Wp.Model.model -> string
      val get_descr : Wp.Model.model -> string
      val get_emitter : Wp.Model.model -> Emitter.t
      val get_separation : Wp.Model.model -> Wp.Model.separation
      val find : id:string -> Wp.Model.model
      val iter : (Wp.Model.model -> unit) -> unit
      val with_model : Wp.Model.model -> ('-> 'b) -> '-> 'b
      val on_model : Wp.Model.model -> (unit -> unit) -> unit
      val get_model : unit -> Wp.Model.model
      val is_model_defined : unit -> bool
      type scope = Kernel_function.t option
      val on_scope : Wp.Model.scope -> ('-> 'b) -> '-> 'b
      val on_kf : Kernel_function.t -> (unit -> unit) -> unit
      val on_global : (unit -> unit) -> unit
      val get_scope : unit -> Wp.Model.scope
      val directory : unit -> string
      module type Entries =
        sig
          type key
          type data
          val name : string
          val compare : Wp.Model.Entries.key -> Wp.Model.Entries.key -> int
          val pretty : Format.formatter -> Wp.Model.Entries.key -> unit
        end
      module type Registry =
        sig
          module E : Entries
          type key = E.key
          type data = E.data
          val mem : Wp.Model.Registry.key -> bool
          val find : Wp.Model.Registry.key -> Wp.Model.Registry.data
          val get : Wp.Model.Registry.key -> Wp.Model.Registry.data option
          val define :
            Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit
          val update :
            Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit
          val memoize :
            (Wp.Model.Registry.key -> Wp.Model.Registry.data) ->
            Wp.Model.Registry.key -> Wp.Model.Registry.data
          val compile :
            (Wp.Model.Registry.key -> Wp.Model.Registry.data) ->
            Wp.Model.Registry.key -> unit
          val callback :
            (Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit) -> unit
          val iter :
            (Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit) -> unit
          val iter_sorted :
            (Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit) -> unit
        end
      module Index :
        functor (E : Entries->
          sig
            module E :
              sig
                type key = E.key
                type data = E.data
                val name : string
                val compare : key -> key -> int
                val pretty : Format.formatter -> key -> unit
              end
            type key = E.key
            type data = E.data
            val mem : key -> bool
            val find : key -> data
            val get : key -> data option
            val define : key -> data -> unit
            val update : key -> data -> unit
            val memoize : (key -> data) -> key -> data
            val compile : (key -> data) -> key -> unit
            val callback : (key -> data -> unit) -> unit
            val iter : (key -> data -> unit) -> unit
            val iter_sorted : (key -> data -> unit) -> unit
          end
      module Static :
        functor (E : Entries->
          sig
            module E :
              sig
                type key = E.key
                type data = E.data
                val name : string
                val compare : key -> key -> int
                val pretty : Format.formatter -> key -> unit
              end
            type key = E.key
            type data = E.data
            val mem : key -> bool
            val find : key -> data
            val get : key -> data option
            val define : key -> data -> unit
            val update : key -> data -> unit
            val memoize : (key -> data) -> key -> data
            val compile : (key -> data) -> key -> unit
            val callback : (key -> data -> unit) -> unit
            val iter : (key -> data -> unit) -> unit
            val iter_sorted : (key -> data -> unit) -> unit
          end
      module type Key =
        sig
          type t
          val compare : Wp.Model.Key.t -> Wp.Model.Key.t -> int
          val pretty : Format.formatter -> Wp.Model.Key.t -> unit
        end
      module type Data =
        sig
          type key
          type data
          val name : string
          val compile : Wp.Model.Data.key -> Wp.Model.Data.data
        end
      module type Generator =
        sig
          type key
          type data
          val get : Wp.Model.Generator.key -> Wp.Model.Generator.data
        end
      module Generator :
        functor
          (K : Key) (D : sig
                           type key = K.t
                           type data
                           val name : string
                           val compile : key -> data
                         end->
          sig type key = D.key type data = D.data val get : key -> data end
      module StaticGenerator :
        functor
          (K : Key) (D : sig
                           type key = K.t
                           type data
                           val name : string
                           val compile : key -> data
                         end->
          sig type key = D.key type data = D.data val get : key -> data end
    end
  module Lang :
    sig
      type library = string
      type 'a infoprover = { altergo : 'a; why3 : 'a; coq : 'a; }
      val infoprover : '-> 'Wp.Lang.infoprover
      val comp_id : Cil_types.compinfo -> string
      val field_id : Cil_types.fieldinfo -> string
      val type_id : Cil_types.logic_type_info -> string
      val logic_id : Cil_types.logic_info -> string
      val lemma_id : string -> string
      type adt = private
          Mtype of Wp.Lang.mdt
        | Mrecord of Wp.Lang.mdt * Wp.Lang.fields
        | Atype of Cil_types.logic_type_info
        | Comp of Cil_types.compinfo
      and mdt = string Wp.Lang.extern
      and 'a extern = {
        ext_id : int;
        ext_link : 'Wp.Lang.infoprover;
        ext_library : Wp.Lang.library;
        ext_debug : string;
      }
      and fields = { mutable fields : Wp.Lang.field list; }
      and field =
          Mfield of Wp.Lang.mdt * Wp.Lang.fields * string * Wp.Lang.tau
        | Cfield of Cil_types.fieldinfo
      and tau = (Wp.Lang.field, Wp.Lang.adt) Qed.Logic.datatype
      type lfun =
          ACSL of Cil_types.logic_info
        | CTOR of Cil_types.logic_ctor_info
        | Model of Wp.Lang.model
      and model = {
        m_category : Wp.Lang.lfun Qed.Logic.category;
        m_params : Qed.Logic.sort list;
        m_resort : Qed.Logic.sort;
        m_result : Wp.Lang.tau option;
        m_source : Wp.Lang.source;
      }
      and source =
          Generated of string
        | Extern of Qed.Engine.link Wp.Lang.extern
      val builtin_type :
        name:string ->
        link:string Wp.Lang.infoprover -> library:string -> unit
      val is_builtin_type : name:string -> Wp.Lang.tau -> bool
      val datatype : library:string -> string -> Wp.Lang.adt
      val record :
        link:string Wp.Lang.infoprover ->
        library:string -> (string * Wp.Lang.tau) list -> Wp.Lang.adt
      val atype : Cil_types.logic_type_info -> Wp.Lang.adt
      val comp : Cil_types.compinfo -> Wp.Lang.adt
      val field : Wp.Lang.adt -> string -> Wp.Lang.field
      val fields_of_tau : Wp.Lang.tau -> Wp.Lang.field list
      val fields_of_field : Wp.Lang.field -> Wp.Lang.field list
      type balance = Nary | Left | Right
      val extern_s :
        library:Wp.Lang.library ->
        ?link:Qed.Engine.link Wp.Lang.infoprover ->
        ?category:Wp.Lang.lfun Qed.Logic.category ->
        ?params:Qed.Logic.sort list ->
        ?sort:Qed.Logic.sort -> ?result:Wp.Lang.tau -> string -> Wp.Lang.lfun
      val extern_f :
        library:Wp.Lang.library ->
        ?link:Qed.Engine.link Wp.Lang.infoprover ->
        ?balance:Wp.Lang.balance ->
        ?category:Wp.Lang.lfun Qed.Logic.category ->
        ?params:Qed.Logic.sort list ->
        ?sort:Qed.Logic.sort ->
        ?result:Wp.Lang.tau ->
        ('a, Format.formatter, unit, Wp.Lang.lfun) Pervasives.format4 -> 'a
      val extern_p :
        library:Wp.Lang.library ->
        ?bool:string ->
        ?prop:string ->
        ?link:Qed.Engine.link Wp.Lang.infoprover ->
        ?params:Qed.Logic.sort list -> unit -> Wp.Lang.lfun
      val extern_fp :
        library:Wp.Lang.library ->
        ?params:Qed.Logic.sort list ->
        ?link:string Wp.Lang.infoprover -> string -> Wp.Lang.lfun
      val generated_f :
        ?category:Wp.Lang.lfun Qed.Logic.category ->
        ?params:Qed.Logic.sort list ->
        ?sort:Qed.Logic.sort ->
        ?result:Wp.Lang.tau ->
        ('a, Format.formatter, unit, Wp.Lang.lfun) Pervasives.format4 -> 'a
      val generated_p : string -> Wp.Lang.lfun
      val tau_of_comp : Cil_types.compinfo -> Wp.Lang.tau
      val tau_of_object : Wp.Ctypes.c_object -> Wp.Lang.tau
      val tau_of_ctype : Cil_types.typ -> Wp.Lang.tau
      val tau_of_ltype : Cil_types.logic_type -> Wp.Lang.tau
      val tau_of_return : Cil_types.logic_info -> Wp.Lang.tau
      val tau_of_lfun : Wp.Lang.lfun -> Wp.Lang.tau
      val tau_of_field : Wp.Lang.field -> Wp.Lang.tau
      val tau_of_record : Wp.Lang.field -> Wp.Lang.tau
      val array : Wp.Lang.tau -> Wp.Lang.tau
      val farray : Wp.Lang.tau -> Wp.Lang.tau -> Wp.Lang.tau
      val pointer : (Cil_types.typ -> Wp.Lang.tau) Wp.Context.value
      val poly : string list Wp.Context.value
      val parameters : (Wp.Lang.lfun -> Qed.Logic.sort list) -> unit
      module ADT :
        sig
          type t = adt
          val hash : t -> int
          val equal : t -> t -> bool
          val compare : t -> t -> int
          val pretty : Format.formatter -> t -> unit
          val debug : t -> string
          val basename : t -> string
        end
      module Field :
        sig
          type t = field
          val hash : t -> int
          val equal : t -> t -> bool
          val compare : t -> t -> int
          val pretty : Format.formatter -> t -> unit
          val debug : t -> string
          val sort : t -> Qed.Logic.sort
        end
      module Fun :
        sig
          type t = lfun
          val hash : t -> int
          val equal : t -> t -> bool
          val compare : t -> t -> int
          val pretty : Format.formatter -> t -> unit
          val debug : t -> string
          val category : t -> t Qed.Logic.category
          val params : t -> Qed.Logic.sort list
          val sort : t -> Qed.Logic.sort
        end
      class virtual idprinting :
        object
          method virtual basename : string -> string
          method datatype : Wp.Lang.ADT.t -> string
          method datatypename : string -> string
          method field : Wp.Lang.Field.t -> string
          method fieldname : string -> string
          method funname : string -> string
          method virtual infoprover : 'Wp.Lang.infoprover -> 'a
          method link : Wp.Lang.Fun.t -> Qed.Engine.link
        end
      module F :
        sig
          module Z :
            sig
              type t = Integer.t
              val zero : t
              val one : t
              val minus_one : t
              val succ : t -> t
              val pred : t -> t
              val neg : t -> t
              val add : t -> t -> t
              val sub : t -> t -> t
              val mul : t -> t -> t
              val div : t -> t -> t
              val rem : t -> t -> t
              val div_rem : t -> t -> t * t
              val equal : t -> t -> bool
              val leq : t -> t -> bool
              val lt : t -> t -> bool
              val of_int : int -> t
              val of_string : string -> t
              val to_string : t -> string
              val hash : t -> int
              val compare : t -> t -> int
            end
          module ADT :
            sig
              type t = adt
              val hash : t -> int
              val equal : t -> t -> bool
              val compare : t -> t -> int
              val pretty : Format.formatter -> t -> unit
              val debug : t -> string
              val basename : t -> string
            end
          module Field :
            sig
              type t = field
              val hash : t -> int
              val equal : t -> t -> bool
              val compare : t -> t -> int
              val pretty : Format.formatter -> t -> unit
              val debug : t -> string
              val sort : t -> Qed.Logic.sort
            end
          module Fun :
            sig
              type t = lfun
              val hash : t -> int
              val equal : t -> t -> bool
              val compare : t -> t -> int
              val pretty : Format.formatter -> t -> unit
              val debug : t -> string
              val category : t -> t Qed.Logic.category
              val params : t -> Qed.Logic.sort list
              val sort : t -> Qed.Logic.sort
            end
          module Var : Qed.Logic.Variable
          type term
          type bind
          type var = Var.t
          type tau = (Field.t, ADT.t) Qed.Logic.datatype
          type signature = (Field.t, ADT.t) Qed.Logic.funtype
          module Tau :
            sig
              type t = tau
              val hash : t -> int
              val equal : t -> t -> bool
              val compare : t -> t -> int
              val pretty : Format.formatter -> t -> unit
              val debug : t -> string
              val basename : t -> string
            end
          module Vars :
            sig
              type elt = var
              type 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 Vmap :
            sig
              type key = var
              type 'a t
              val is_empty : 'a t -> bool
              val empty : 'a t
              val add : key -> '-> 'a t -> 'a t
              val mem : key -> 'a t -> bool
              val find : key -> 'a t -> 'a
              val remove : key -> 'a t -> 'a 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 map : (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 fold : (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 merge :
                (key -> 'a option -> 'b option -> 'c option) ->
                'a t -> 'b t -> 'c t
              val insert :
                (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
              val change :
                (key -> '-> 'a option -> 'a option) ->
                key -> '-> 'a t -> 'a t
            end
          type pool
          val pool : ?copy:pool -> unit -> pool
          val add_var : pool -> var -> unit
          val add_vars : pool -> Vars.t -> unit
          val add_term : pool -> term -> unit
          val fresh : pool -> ?basename:string -> tau -> var
          val alpha : pool -> var -> var
          val tau_of_var : var -> tau
          val sort_of_var : var -> Qed.Logic.sort
          val base_of_var : var -> string
          type 'a expression =
              (Z.t, Field.t, ADT.t, Fun.t, var, bind, 'a) Qed.Logic.term_repr
          type repr = term expression
          type path = int list
          type record = (Field.t * term) list
          val decide : term -> bool
          val is_true : term -> Qed.Logic.maybe
          val is_false : term -> Qed.Logic.maybe
          val is_prop : term -> bool
          val is_int : term -> bool
          val is_real : term -> bool
          val is_arith : term -> bool
          val are_equal : term -> term -> Qed.Logic.maybe
          val eval_eq : term -> term -> bool
          val eval_neq : term -> term -> bool
          val eval_lt : term -> term -> bool
          val eval_leq : term -> term -> bool
          val repr : term -> repr
          val sort : term -> Qed.Logic.sort
          val vars : term -> Vars.t
          val subterm : term -> path -> term
          val change_subterm : term -> path -> term -> term
          val e_true : term
          val e_false : term
          val e_bool : bool -> term
          val e_literal : bool -> term -> term
          val e_int : int -> term
          val e_zint : Z.t -> term
          val e_real : Qed.R.t -> term
          val e_var : var -> term
          val e_opp : term -> term
          val e_times : Z.t -> term -> term
          val e_sum : term list -> term
          val e_prod : term list -> term
          val e_add : term -> term -> term
          val e_sub : term -> term -> term
          val e_mul : term -> term -> term
          val e_div : term -> term -> term
          val e_mod : term -> term -> term
          val e_eq : term -> term -> term
          val e_neq : term -> term -> term
          val e_leq : term -> term -> term
          val e_lt : term -> term -> term
          val e_imply : term list -> term -> term
          val e_equiv : term -> term -> term
          val e_and : term list -> term
          val e_or : term list -> term
          val e_not : term -> term
          val e_if : term -> term -> term -> term
          val e_get : term -> term -> term
          val e_set : term -> term -> term -> term
          val e_getfield : term -> Field.t -> term
          val e_record : record -> term
          val e_fun : Fun.t -> term list -> term
          val e_repr : repr -> term
          val e_forall : var list -> term -> term
          val e_exists : var list -> term -> term
          val e_lambda : var list -> term -> term
          val e_bind : Qed.Logic.binder -> var -> term -> term
          val e_apply : term -> term list -> term
          type sigma
          val sigma : unit -> sigma
          val e_subst_var : var -> term -> term -> term
          val lc_bind : var -> term -> bind
          val lc_open : var -> bind -> term
          val lc_open_term : term -> bind -> term
          val lc_closed : term -> bool
          val lc_closed_at : int -> term -> bool
          val lc_vars : term -> Qed.Bvars.t
          val lc_repr : bind -> term
          val e_map : pool -> (term -> term) -> term -> term
          val e_iter : pool -> (term -> unit) -> term -> unit
          val f_map : (int -> term -> term) -> int -> term -> term
          val f_iter : (int -> term -> unit) -> int -> term -> unit
          val lc_map : (term -> term) -> term -> term
          val lc_iter : (term -> unit) -> term -> unit
          val set_builtin : Fun.t -> (term list -> term) -> unit
          val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
          val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit
          val literal : term -> bool * term
          val congruence_eq : term -> term -> (term * term) list option
          val congruence_neq : term -> term -> (term * term) list option
          val flattenable : term -> bool
          val flattens : term -> term -> bool
          val flatten : term -> term list
          val affine : term -> (Z.t, term) Qed.Logic.affine
          val record_with : record -> (term * record) option
          type t = term
          val id : t -> int
          val hash : t -> int
          val equal : t -> t -> bool
          val compare : t -> t -> int
          val pretty : Format.formatter -> t -> unit
          val weigth : t -> int
          val is_closed : t -> bool
          val is_simple : t -> bool
          val is_atomic : t -> bool
          val is_primitive : t -> bool
          val is_neutral : Fun.t -> t -> bool
          val is_absorbant : Fun.t -> t -> bool
          val size : t -> int
          val basename : t -> string
          val debug : Format.formatter -> t -> unit
          val pp_id : Format.formatter -> t -> unit
          val pp_rid : Format.formatter -> t -> unit
          val pp_repr : Format.formatter -> repr -> unit
          module Term :
            sig
              type t = term
              val hash : t -> int
              val equal : t -> t -> bool
              val compare : t -> t -> int
              val pretty : Format.formatter -> t -> unit
              val debug : t -> string
            end
          module Tset :
            sig
              type elt = term
              type 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 Tmap :
            sig
              type key = term
              type 'a t
              val is_empty : 'a t -> bool
              val empty : 'a t
              val add : key -> '-> 'a t -> 'a t
              val mem : key -> 'a t -> bool
              val find : key -> 'a t -> 'a
              val remove : key -> 'a t -> 'a 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 map : (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 fold : (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 merge :
                (key -> 'a option -> 'b option -> 'c option) ->
                'a t -> 'b t -> 'c t
              val insert :
                (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
              val change :
                (key -> '-> 'a option -> 'a option) ->
                key -> '-> 'a t -> 'a t
            end
          val shared :
            ?shared:(term -> bool) ->
            ?shareable:(term -> bool) -> term list -> term list
          type marks
          val marks :
            ?shared:(term -> bool) ->
            ?shareable:(term -> bool) -> unit -> marks
          val mark : marks -> term -> unit
          val share : marks -> term -> unit
          val defs : marks -> term list
          type unop = term -> term
          type binop = term -> term -> term
          val e_zero : term
          val e_one : term
          val e_minus_one : term
          val e_one_real : term
          val e_zero_real : term
          val constant : term -> term
          val e_fact : int -> term -> term
          val e_int64 : int64 -> term
          val e_bigint : Integer.t -> term
          val e_mthfloat : float -> term
          val e_hexfloat : float -> term
          val e_setfield : term -> Wp.Lang.field -> term -> term
          val e_range : term -> term -> term
          val is_zero : term -> bool
          type pred
          type cmp = term -> term -> Wp.Lang.F.pred
          val p_true : Wp.Lang.F.pred
          val p_false : Wp.Lang.F.pred
          val p_equal : term -> term -> Wp.Lang.F.pred
          val p_neq : term -> term -> Wp.Lang.F.pred
          val p_leq : term -> term -> Wp.Lang.F.pred
          val p_lt : term -> term -> Wp.Lang.F.pred
          val p_positive : term -> Wp.Lang.F.pred
          val is_ptrue : Wp.Lang.F.pred -> Qed.Logic.maybe
          val is_pfalse : Wp.Lang.F.pred -> Qed.Logic.maybe
          val is_equal : term -> term -> Qed.Logic.maybe
          val eqp : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool
          val comparep : Wp.Lang.F.pred -> Wp.Lang.F.pred -> int
          val p_bool : term -> Wp.Lang.F.pred
          val e_prop : Wp.Lang.F.pred -> term
          val p_bools : term list -> Wp.Lang.F.pred list
          val e_props : Wp.Lang.F.pred list -> term list
          val lift : (term -> term) -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_not : Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_and : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_or : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_imply : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_equiv : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_hyps :
            Wp.Lang.F.pred list -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_if :
            Wp.Lang.F.pred ->
            Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_conj : Wp.Lang.F.pred list -> Wp.Lang.F.pred
          val p_disj : Wp.Lang.F.pred list -> Wp.Lang.F.pred
          val p_any : ('-> Wp.Lang.F.pred) -> 'a list -> Wp.Lang.F.pred
          val p_all : ('-> Wp.Lang.F.pred) -> 'a list -> Wp.Lang.F.pred
          val p_call : Wp.Lang.lfun -> term list -> Wp.Lang.F.pred
          val p_forall : var list -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_exists : var list -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val p_bind :
            Qed.Logic.binder -> var -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
          val p_subst :
            ?sigma:sigma ->
            (term -> term) -> Wp.Lang.F.pred -> Wp.Lang.F.pred
          val e_vars : term -> var list
          val p_vars : Wp.Lang.F.pred -> var list
          val p_close : Wp.Lang.F.pred -> Wp.Lang.F.pred
          val idp : Wp.Lang.F.pred -> int
          val varsp : Wp.Lang.F.pred -> Vars.t
          val occurs : var -> term -> bool
          val occursp : var -> Wp.Lang.F.pred -> bool
          val intersect : term -> term -> bool
          val intersectp : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool
          val pp_tau : Format.formatter -> Wp.Lang.tau -> unit
          val pp_var : Format.formatter -> var -> unit
          val pp_vars : Format.formatter -> Vars.t -> unit
          val pp_term : Format.formatter -> term -> unit
          val pp_pred : Format.formatter -> Wp.Lang.F.pred -> unit
          val debugp : Format.formatter -> Wp.Lang.F.pred -> unit
          type env
          val env : Vars.t -> Wp.Lang.F.env
          val marker : Wp.Lang.F.env -> marks
          val mark_e : marks -> term -> unit
          val mark_p : marks -> Wp.Lang.F.pred -> unit
          val define :
            (Wp.Lang.F.env -> string -> term -> unit) ->
            Wp.Lang.F.env -> marks -> Wp.Lang.F.env
          val pp_eterm : Wp.Lang.F.env -> Format.formatter -> term -> unit
          val pp_epred :
            Wp.Lang.F.env -> Format.formatter -> Wp.Lang.F.pred -> unit
          val pred : Wp.Lang.F.pred -> Wp.Lang.F.pred expression
          val epred : Wp.Lang.F.pred -> term expression
          val p_iter :
            (Wp.Lang.F.pred -> unit) ->
            (term -> unit) -> Wp.Lang.F.pred -> unit
          module Pmap :
            sig
              type key = pred
              type 'a t
              val is_empty : 'a t -> bool
              val empty : 'a t
              val add : key -> '-> 'a t -> 'a t
              val mem : key -> 'a t -> bool
              val find : key -> 'a t -> 'a
              val remove : key -> 'a t -> 'a 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 map : (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 fold : (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 merge :
                (key -> 'a option -> 'b option -> 'c option) ->
                'a t -> 'b t -> 'c t
              val insert :
                (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
              val change :
                (key -> '-> 'a option -> 'a option) ->
                key -> '-> 'a t -> 'a t
            end
          module Pset :
            sig
              type elt = pred
              type 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
          val release : unit -> unit
          val set_builtin_1 : Wp.Lang.lfun -> (term -> term) -> unit
          val set_builtin_2 : Wp.Lang.lfun -> (term -> term -> term) -> unit
          val set_builtin_eqp :
            Wp.Lang.lfun -> (term -> term -> Wp.Lang.F.pred) -> unit
          val do_checks : bool Pervasives.ref
          val iter_checks :
            (qed:term -> raw:term -> goal:Wp.Lang.F.pred -> unit) -> unit
        end
      type gamma
      val new_pool : ?copy:Wp.Lang.F.pool -> unit -> Wp.Lang.F.pool
      val new_gamma : ?copy:Wp.Lang.gamma -> unit -> Wp.Lang.gamma
      val local :
        ?pool:Wp.Lang.F.pool ->
        ?gamma:Wp.Lang.gamma -> ('-> 'b) -> '-> 'b
      val freshvar : ?basename:string -> Wp.Lang.F.tau -> Wp.Lang.F.var
      val freshen : Wp.Lang.F.var -> Wp.Lang.F.var
      val assume : Wp.Lang.F.pred -> unit
      val without_assume : ('-> 'b) -> '-> 'b
      val epsilon :
        ?basename:string ->
        Wp.Lang.F.tau -> (Wp.Lang.F.term -> Wp.Lang.F.pred) -> Wp.Lang.F.term
      val hypotheses : Wp.Lang.gamma -> Wp.Lang.F.pred list
      val variables : Wp.Lang.gamma -> Wp.Lang.F.var list
      val get_pool : unit -> Wp.Lang.F.pool
      val get_gamma : unit -> Wp.Lang.gamma
      val get_hypotheses : unit -> Wp.Lang.F.pred list
      val get_variables : unit -> Wp.Lang.F.var list
      module Alpha :
        sig
          type t
          val create : unit -> Wp.Lang.Alpha.t
          val get : Wp.Lang.Alpha.t -> Wp.Lang.F.var -> Wp.Lang.F.var
          val iter :
            (Wp.Lang.F.var -> Wp.Lang.F.var -> unit) ->
            Wp.Lang.Alpha.t -> unit
          val convert : Wp.Lang.Alpha.t -> Wp.Lang.F.term -> Wp.Lang.F.term
          val convertp : Wp.Lang.Alpha.t -> Wp.Lang.F.pred -> Wp.Lang.F.pred
        end
    end
  module Splitter :
    sig
      type tag =
          MARK of Cil_types.stmt
        | THEN of Cil_types.stmt
        | ELSE of Cil_types.stmt
        | CALL of Cil_types.stmt * Cil_types.kernel_function
        | CASE of Cil_types.stmt * int64 list
        | DEFAULT of Cil_types.stmt
        | ASSERT of Cil_types.identified_predicate * int * int
      val loc : Wp.Splitter.tag -> Cil_types.location
      val pretty : Format.formatter -> Wp.Splitter.tag -> unit
      val mark : Cil_types.stmt -> Wp.Splitter.tag
      val if_then : Cil_types.stmt -> Wp.Splitter.tag
      val if_else : Cil_types.stmt -> Wp.Splitter.tag
      val switch_cases : Cil_types.stmt -> int64 list -> Wp.Splitter.tag
      val switch_default : Cil_types.stmt -> Wp.Splitter.tag
      val cases :
        Cil_types.identified_predicate ->
        (Wp.Splitter.tag * Cil_types.predicate Cil_types.named) list option
      val call :
        Cil_types.stmt -> Cil_types.kernel_function -> Wp.Splitter.tag
      type 'a t
      val empty : 'Wp.Splitter.t
      val singleton : '-> 'Wp.Splitter.t
      val group :
        Wp.Splitter.tag ->
        ('a list -> 'a) -> 'Wp.Splitter.t -> 'Wp.Splitter.t
      val union :
        ('-> '-> 'a) ->
        'Wp.Splitter.t -> 'Wp.Splitter.t -> 'Wp.Splitter.t
      val merge :
        left:('-> 'c) ->
        both:('-> '-> 'c) ->
        right:('-> 'c) ->
        'Wp.Splitter.t -> 'Wp.Splitter.t -> 'Wp.Splitter.t
      val merge_all :
        ('a list -> 'a) -> 'Wp.Splitter.t list -> 'Wp.Splitter.t
      val length : 'Wp.Splitter.t -> int
      val map : ('-> 'b) -> 'Wp.Splitter.t -> 'Wp.Splitter.t
      val iter :
        (Wp.Splitter.tag list -> '-> unit) -> 'Wp.Splitter.t -> unit
      val fold :
        (Wp.Splitter.tag list -> '-> '-> 'b) ->
        'Wp.Splitter.t -> '-> 'b
      val exists : ('-> bool) -> 'Wp.Splitter.t -> bool
      val for_all : ('-> bool) -> 'Wp.Splitter.t -> bool
      val filter : ('-> bool) -> 'Wp.Splitter.t -> 'Wp.Splitter.t
    end
  module Definitions :
    sig
      type cluster
      val cluster :
        id:string ->
        ?title:string ->
        ?position:Lexing.position -> unit -> Wp.Definitions.cluster
      val axiomatic : Wp.LogicUsage.axiomatic -> Wp.Definitions.cluster
      val section : Wp.LogicUsage.logic_section -> Wp.Definitions.cluster
      val compinfo : Cil_types.compinfo -> Wp.Definitions.cluster
      val matrix : Wp.Ctypes.c_object -> Wp.Definitions.cluster
      val cluster_id : Wp.Definitions.cluster -> string
      val cluster_title : Wp.Definitions.cluster -> string
      val cluster_position : Wp.Definitions.cluster -> Lexing.position option
      val cluster_age : Wp.Definitions.cluster -> int
      val cluster_compare :
        Wp.Definitions.cluster -> Wp.Definitions.cluster -> int
      val pp_cluster : Format.formatter -> Wp.Definitions.cluster -> unit
      val iter : (Wp.Definitions.cluster -> unit) -> unit
      type trigger = (Wp.Lang.F.var, Wp.Lang.lfun) Qed.Engine.ftrigger
      type typedef =
          (Wp.Lang.F.tau, Wp.Lang.field, Wp.Lang.lfun) Qed.Engine.ftypedef
      type dlemma = {
        l_name : string;
        l_cluster : Wp.Definitions.cluster;
        l_assumed : bool;
        l_types : int;
        l_forall : Wp.Lang.F.var list;
        l_triggers : Wp.Definitions.trigger list list;
        l_lemma : Wp.Lang.F.pred;
      }
      type definition =
          Logic of Wp.Lang.F.tau
        | Value of Wp.Lang.F.tau * Wp.Definitions.recursion * Wp.Lang.F.term
        | Predicate of Wp.Definitions.recursion * Wp.Lang.F.pred
        | Inductive of Wp.Definitions.dlemma list
      and recursion = Def | Rec
      type dfun = {
        d_lfun : Wp.Lang.lfun;
        d_cluster : Wp.Definitions.cluster;
        d_types : int;
        d_params : Wp.Lang.F.var list;
        d_definition : Wp.Definitions.definition;
      }
      module Trigger :
        sig
          val of_term : Wp.Lang.F.term -> Wp.Definitions.trigger
          val of_pred : Wp.Lang.F.pred -> Wp.Definitions.trigger
          val vars : Wp.Definitions.trigger -> Wp.Lang.F.Vars.t
        end
      val define_symbol : Wp.Definitions.dfun -> unit
      val update_symbol : Wp.Definitions.dfun -> unit
      val find_lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
      val compile_lemma :
        (Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma) ->
        Wp.LogicUsage.logic_lemma -> unit
      val define_lemma : Wp.Definitions.dlemma -> unit
      val define_type :
        Wp.Definitions.cluster -> Cil_types.logic_type_info -> unit
      val call_fun :
        Wp.Lang.lfun ->
        (Wp.Lang.lfun -> Wp.Definitions.dfun) ->
        Wp.Lang.F.term list -> Wp.Lang.F.term
      val call_pred :
        Wp.Lang.lfun ->
        (Wp.Lang.lfun -> Wp.Definitions.dfun) ->
        Wp.Lang.F.term list -> Wp.Lang.F.pred
      type axioms = Wp.Definitions.cluster * Wp.LogicUsage.logic_lemma list
      class virtual visitor :
        Wp.Definitions.cluster ->
        object
          method do_local : Wp.Definitions.cluster -> bool
          method virtual on_cluster : Wp.Definitions.cluster -> unit
          method virtual on_comp :
            Cil_types.compinfo ->
            (Wp.Lang.field * Wp.Lang.F.tau) list -> unit
          method virtual on_dfun : Wp.Definitions.dfun -> unit
          method virtual on_dlemma : Wp.Definitions.dlemma -> unit
          method virtual on_library : string -> unit
          method virtual on_type :
            Cil_types.logic_type_info -> Wp.Definitions.typedef -> unit
          method virtual section : string -> unit
          method set_local : Wp.Definitions.cluster -> unit
          method vadt : Wp.Lang.F.ADT.t -> unit
          method vcluster : Wp.Definitions.cluster -> unit
          method vcomp : Cil_types.compinfo -> unit
          method vfield : Wp.Lang.F.Field.t -> unit
          method vgoal :
            Wp.Definitions.axioms option -> Wp.Lang.F.pred -> unit
          method vlemma : Wp.LogicUsage.logic_lemma -> unit
          method vlibrary : string -> unit
          method vparam : Wp.Lang.F.var -> unit
          method vpred : Wp.Lang.F.pred -> unit
          method vself : unit
          method vsymbol : Wp.Lang.lfun -> unit
          method vtau : Wp.Lang.F.tau -> unit
          method vterm : Wp.Lang.F.term -> unit
          method vtype : Cil_types.logic_type_info -> unit
        end
    end
  module Conditions :
    sig
      type step = private {
        size : int;
        vars : Wp.Lang.F.Vars.t;
        stmt : Cil_types.stmt option;
        descr : string option;
        deps : Property.t list;
        warn : Wp.Warning.Set.t;
        condition : Wp.Conditions.condition;
      }
      and condition =
          Type of Wp.Lang.F.pred
        | Have of Wp.Lang.F.pred
        | When of Wp.Lang.F.pred
        | Core of Wp.Lang.F.pred
        | Init of Wp.Lang.F.pred
        | Branch of Wp.Lang.F.pred * Wp.Conditions.sequence *
            Wp.Conditions.sequence
        | Either of Wp.Conditions.sequence list
      and sequence
      type sequent = Wp.Conditions.sequence * Wp.Lang.F.pred
      val step :
        ?descr:string ->
        ?stmt:Cil_types.stmt ->
        ?deps:Property.t list ->
        ?warn:Wp.Warning.Set.t ->
        Wp.Conditions.condition -> Wp.Conditions.step
      val is_empty : Wp.Conditions.sequence -> bool
      val vars_hyp : Wp.Conditions.sequence -> Wp.Lang.F.Vars.t
      val vars_seq : Wp.Conditions.sequent -> Wp.Lang.F.Vars.t
      val empty : Wp.Conditions.sequence
      val seq_list : Wp.Conditions.step list -> Wp.Conditions.sequence
      val seq_branch :
        ?stmt:Cil_types.stmt ->
        Wp.Lang.F.pred ->
        Wp.Conditions.sequence ->
        Wp.Conditions.sequence -> Wp.Conditions.sequence
      val append :
        Wp.Conditions.sequence ->
        Wp.Conditions.sequence -> Wp.Conditions.sequence
      val concat : Wp.Conditions.sequence list -> Wp.Conditions.sequence
      val iter :
        (Wp.Conditions.step -> unit) -> Wp.Conditions.sequence -> unit
      val iteri :
        ?from:int ->
        (int -> Wp.Conditions.step -> unit) -> Wp.Conditions.sequence -> unit
      val condition : Wp.Conditions.sequence -> Wp.Lang.F.pred
      val close : Wp.Conditions.sequent -> Wp.Lang.F.pred
      type bundle
      type 'a attributed =
          ?descr:string ->
          ?stmt:Cil_types.stmt ->
          ?deps:Property.t list -> ?warn:Wp.Warning.Set.t -> 'a
      val nil : Wp.Conditions.bundle
      val occurs : Wp.Lang.F.var -> Wp.Conditions.bundle -> bool
      val intersect : Wp.Lang.F.pred -> Wp.Conditions.bundle -> bool
      val merge : Wp.Conditions.bundle list -> Wp.Conditions.bundle
      val domain :
        Wp.Lang.F.pred list -> Wp.Conditions.bundle -> Wp.Conditions.bundle
      val intros :
        Wp.Lang.F.pred list -> Wp.Conditions.bundle -> Wp.Conditions.bundle
      val assume :
        (?init:bool ->
         Wp.Lang.F.pred -> Wp.Conditions.bundle -> Wp.Conditions.bundle)
        Wp.Conditions.attributed
      val branch :
        (Wp.Lang.F.pred ->
         Wp.Conditions.bundle -> Wp.Conditions.bundle -> Wp.Conditions.bundle)
        Wp.Conditions.attributed
      val either :
        (Wp.Conditions.bundle list -> Wp.Conditions.bundle)
        Wp.Conditions.attributed
      val extract : Wp.Conditions.bundle -> Wp.Lang.F.pred list
      val sequence : Wp.Conditions.bundle -> Wp.Conditions.sequence
      exception Contradiction
      class type simplifier =
        object
          method assume : Wp.Lang.F.pred -> unit
          method copy : Wp.Conditions.simplifier
          method fixpoint : unit
          method infer : Wp.Lang.F.pred list
          method name : string
          method simplify_branch : Wp.Lang.F.pred -> Wp.Lang.F.pred
          method simplify_goal : Wp.Lang.F.pred -> Wp.Lang.F.pred
          method simplify_hyp : Wp.Lang.F.pred -> Wp.Lang.F.pred
          method target : Wp.Lang.F.pred -> unit
        end
      val clean : Wp.Conditions.sequent -> Wp.Conditions.sequent
      val filter : Wp.Conditions.sequent -> Wp.Conditions.sequent
      val letify :
        ?solvers:Wp.Conditions.simplifier list ->
        Wp.Conditions.sequent -> Wp.Conditions.sequent
      val pruning :
        ?solvers:Wp.Conditions.simplifier list ->
        Wp.Conditions.sequent -> Wp.Conditions.sequent
    end
  module LogicBuiltins :
    sig
      type category = Wp.Lang.lfun Qed.Logic.category
      type kind = Z | R | I of Wp.Ctypes.c_int | F of Wp.Ctypes.c_float | A
      val add_builtin :
        string -> Wp.LogicBuiltins.kind list -> Wp.Lang.lfun -> unit
      type driver
      val driver : Wp.LogicBuiltins.driver Wp.Context.value
      val create :
        id:string ->
        ?descr:string ->
        ?includes:string list -> unit -> Wp.LogicBuiltins.driver
      val init :
        id:string -> ?descr:string -> ?includes:string list -> unit -> unit
      val id : Wp.LogicBuiltins.driver -> string
      val descr : Wp.LogicBuiltins.driver -> string
      val is_default : Wp.LogicBuiltins.driver -> bool
      val compare : Wp.LogicBuiltins.driver -> Wp.LogicBuiltins.driver -> int
      val find_lib : string -> string
      val dependencies : string -> string list
      val add_library : string -> string list -> unit
      val add_alias :
        string -> Wp.LogicBuiltins.kind list -> alias:string -> unit -> unit
      val add_type :
        string ->
        library:string -> ?link:string Wp.Lang.infoprover -> unit -> unit
      val add_ctor :
        string ->
        Wp.LogicBuiltins.kind list ->
        library:string ->
        link:Qed.Engine.link Wp.Lang.infoprover -> unit -> unit
      val add_logic :
        Wp.LogicBuiltins.kind ->
        string ->
        Wp.LogicBuiltins.kind list ->
        library:string ->
        ?category:Wp.LogicBuiltins.category ->
        link:Qed.Engine.link Wp.Lang.infoprover -> unit -> unit
      val add_predicate :
        string ->
        Wp.LogicBuiltins.kind list ->
        library:string -> link:string Wp.Lang.infoprover -> unit -> unit
      val add_option :
        driver_dir:string ->
        string -> string -> library:string -> string -> unit
      val set_option :
        driver_dir:string ->
        string -> string -> library:string -> string -> unit
      type doption
      val create_option :
        (driver_dir:string -> string -> string) ->
        string -> string -> Wp.LogicBuiltins.doption
      val get_option :
        Wp.LogicBuiltins.doption -> library:string -> string list
      type builtin = ACSLDEF | LFUN of Wp.Lang.lfun
      val logic : Cil_types.logic_info -> Wp.LogicBuiltins.builtin
      val ctor : Cil_types.logic_ctor_info -> Wp.LogicBuiltins.builtin
      val constant : string -> Wp.LogicBuiltins.builtin
      val dump : unit -> unit
    end
  module Vset :
    sig
      type set = Wp.Vset.vset list
      and vset =
          Set of Wp.Lang.F.tau * Wp.Lang.F.term
        | Singleton of Wp.Lang.F.term
        | Range of Wp.Lang.F.term option * Wp.Lang.F.term option
        | Descr of Wp.Lang.F.var list * Wp.Lang.F.term * Wp.Lang.F.pred
      val tau_of_set : Wp.Lang.F.tau -> Wp.Lang.F.tau
      val vars : Wp.Vset.set -> Wp.Lang.F.Vars.t
      val occurs : Wp.Lang.F.var -> Wp.Vset.set -> bool
      val empty : Wp.Vset.set
      val singleton : Wp.Lang.F.term -> Wp.Vset.set
      val range :
        Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Vset.set
      val union : Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
      val inter : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
      val member : Wp.Lang.F.term -> Wp.Vset.set -> Wp.Lang.F.pred
      val in_size : Wp.Lang.F.term -> int -> Wp.Lang.F.pred
      val in_range :
        Wp.Lang.F.term ->
        Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.pred
      val sub_range :
        Wp.Lang.F.term ->
        Wp.Lang.F.term ->
        Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.pred
      val ordered :
        limit:bool ->
        strict:bool ->
        Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.pred
      val equal : Wp.Vset.set -> Wp.Vset.set -> Wp.Lang.F.pred
      val subset : Wp.Vset.set -> Wp.Vset.set -> Wp.Lang.F.pred
      val disjoint : Wp.Vset.set -> Wp.Vset.set -> Wp.Lang.F.pred
      val concretize : Wp.Vset.set -> Wp.Lang.F.term
      val bound_shift :
        Wp.Lang.F.term option -> Wp.Lang.F.term -> Wp.Lang.F.term option
      val bound_add :
        Wp.Lang.F.term option ->
        Wp.Lang.F.term option -> Wp.Lang.F.term option
      val bound_sub :
        Wp.Lang.F.term option ->
        Wp.Lang.F.term option -> Wp.Lang.F.term option
      val pp_bound : Format.formatter -> Wp.Lang.F.term option -> unit
      val pp_vset : Format.formatter -> Wp.Vset.vset -> unit
      val map :
        (Wp.Lang.F.term -> Wp.Lang.F.term) -> Wp.Vset.set -> Wp.Vset.set
      val map_opp : Wp.Vset.set -> Wp.Vset.set
      val lift :
        (Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term) ->
        Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
      val lift_add : Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
      val lift_sub : Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
      val descr :
        Wp.Vset.vset -> Wp.Lang.F.var list * Wp.Lang.F.term * Wp.Lang.F.pred
    end
  module Cstring :
    sig
      type cst = C_str of string | W_str of int64 list
      val pretty : Format.formatter -> Wp.Cstring.cst -> unit
      val str_len : Wp.Cstring.cst -> Wp.Lang.F.term -> Wp.Lang.F.pred
      val str_val : Wp.Cstring.cst -> Wp.Lang.F.term
      val str_id : Wp.Cstring.cst -> int
      val char_at : Wp.Cstring.cst -> Wp.Lang.F.term -> Wp.Lang.F.term
      val cluster : unit -> Wp.Definitions.cluster
    end
  module Passive :
    sig
      type t
      val empty : Wp.Passive.t
      val union : Wp.Passive.t -> Wp.Passive.t -> Wp.Passive.t
      val bind :
        fresh:Wp.Lang.F.var ->
        bound:Wp.Lang.F.var -> Wp.Passive.t -> Wp.Passive.t
      val join :
        Wp.Lang.F.var -> Wp.Lang.F.var -> Wp.Passive.t -> Wp.Passive.t
      val conditions :
        Wp.Passive.t -> (Wp.Lang.F.var -> bool) -> Wp.Lang.F.pred list
      val apply : Wp.Passive.t -> Wp.Lang.F.pred -> Wp.Lang.F.pred
      val pretty : Format.formatter -> Wp.Passive.t -> unit
    end
  module Memory :
    sig
      type 'a sequence = { pre : 'a; post : 'a; }
      type acs = RW | RD
      type 'a value = Val of Wp.Lang.F.term | Loc of 'a
      type 'a rloc =
          Rloc of Wp.Ctypes.c_object * 'a
        | Rarray of 'a * Wp.Ctypes.c_object * int
        | Rrange of 'a * Wp.Ctypes.c_object * Wp.Lang.F.term option *
            Wp.Lang.F.term option
      type 'a sloc =
          Sloc of 'a
        | Sarray of 'a * Wp.Ctypes.c_object * int
        | Srange of 'a * Wp.Ctypes.c_object * Wp.Lang.F.term option *
            Wp.Lang.F.term option
        | Sdescr of Wp.Lang.F.var list * 'a * Wp.Lang.F.pred
      type 'a logic =
          Vexp of Wp.Lang.F.term
        | Vloc of 'a
        | Vset of Wp.Vset.set
        | Lset of 'Wp.Memory.sloc list
      module type Chunk =
        sig
          type t
          val self : string
          val hash : Wp.Memory.Chunk.t -> int
          val compare : Wp.Memory.Chunk.t -> Wp.Memory.Chunk.t -> int
          val pretty : Format.formatter -> Wp.Memory.Chunk.t -> unit
          val tau_of_chunk : Wp.Memory.Chunk.t -> Wp.Lang.F.tau
          val basename_of_chunk : Wp.Memory.Chunk.t -> string
          val is_framed : Wp.Memory.Chunk.t -> bool
        end
      module type Sigma =
        sig
          type chunk
          type domain
          type t
          val create : unit -> Wp.Memory.Sigma.t
          val copy : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t
          val merge :
            Wp.Memory.Sigma.t ->
            Wp.Memory.Sigma.t ->
            Wp.Memory.Sigma.t * Wp.Passive.t * Wp.Passive.t
          val join : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t -> Wp.Passive.t
          val assigned :
            Wp.Memory.Sigma.t ->
            Wp.Memory.Sigma.t ->
            Wp.Memory.Sigma.domain -> Wp.Lang.F.pred Bag.t
          val mem : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> bool
          val get :
            Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Lang.F.var
          val value :
            Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Lang.F.term
          val iter :
            (Wp.Memory.Sigma.chunk -> Wp.Lang.F.var -> unit) ->
            Wp.Memory.Sigma.t -> unit
          val iter2 :
            (Wp.Memory.Sigma.chunk ->
             Wp.Lang.F.var option -> Wp.Lang.F.var option -> unit) ->
            Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t -> unit
          val havoc :
            Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain -> Wp.Memory.Sigma.t
          val havoc_chunk :
            Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Memory.Sigma.t
          val havoc_any : call:bool -> Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t
          val domain : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain
          val pretty : Format.formatter -> Wp.Memory.Sigma.t -> unit
        end
      module type Model =
        sig
          val configure : Wp.Model.tuning
          val datatype : string
          val separation : unit -> Wp.Separation.clause list
          module Chunk : Chunk
          module Heap :
            sig
              type t = Chunk.t
              type set
              type 'a 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 Sigma :
            sig
              type chunk = Chunk.t
              type domain = Heap.set
              type t
              val create : unit -> t
              val copy : t -> t
              val merge : t -> t -> t * Passive.t * Passive.t
              val join : t -> t -> Passive.t
              val assigned : t -> t -> domain -> Lang.F.pred Bag.t
              val mem : t -> chunk -> bool
              val get : t -> chunk -> Lang.F.var
              val value : t -> chunk -> Lang.F.term
              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 : t -> domain -> t
              val havoc_chunk : t -> chunk -> t
              val havoc_any : call:bool -> t -> t
              val domain : t -> domain
              val pretty : Format.formatter -> t -> unit
            end
          type loc
          type chunk = Wp.Memory.Chunk.t
          type sigma = Wp.Memory.Model.Sigma.t
          type segment = Wp.Memory.Model.loc Wp.Memory.rloc
          val pretty : Format.formatter -> Wp.Memory.Model.loc -> unit
          val vars : Wp.Memory.Model.loc -> Wp.Lang.F.Vars.t
          val occurs : Wp.Lang.F.var -> Wp.Memory.Model.loc -> bool
          val null : Wp.Memory.Model.loc
          val literal : eid:int -> Wp.Cstring.cst -> Wp.Memory.Model.loc
          val cvar : Cil_types.varinfo -> Wp.Memory.Model.loc
          val pointer_loc : Wp.Lang.F.term -> Wp.Memory.Model.loc
          val pointer_val : Wp.Memory.Model.loc -> Wp.Lang.F.term
          val field :
            Wp.Memory.Model.loc -> Cil_types.fieldinfo -> Wp.Memory.Model.loc
          val shift :
            Wp.Memory.Model.loc ->
            Wp.Ctypes.c_object -> Wp.Lang.F.term -> Wp.Memory.Model.loc
          val base_addr : Wp.Memory.Model.loc -> Wp.Memory.Model.loc
          val block_length :
            Wp.Memory.Model.sigma ->
            Wp.Ctypes.c_object -> Wp.Memory.Model.loc -> Wp.Lang.F.term
          val cast :
            Wp.Ctypes.c_object Wp.Memory.sequence ->
            Wp.Memory.Model.loc -> Wp.Memory.Model.loc
          val loc_of_int :
            Wp.Ctypes.c_object -> Wp.Lang.F.term -> Wp.Memory.Model.loc
          val int_of_loc :
            Wp.Ctypes.c_int -> Wp.Memory.Model.loc -> Wp.Lang.F.term
          val domain :
            Wp.Ctypes.c_object ->
            Wp.Memory.Model.loc -> Wp.Memory.Model.Heap.set
          val load :
            Wp.Memory.Model.sigma ->
            Wp.Ctypes.c_object ->
            Wp.Memory.Model.loc -> Wp.Memory.Model.loc Wp.Memory.value
          val copied :
            Wp.Memory.Model.sigma Wp.Memory.sequence ->
            Wp.Ctypes.c_object ->
            Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred list
          val stored :
            Wp.Memory.Model.sigma Wp.Memory.sequence ->
            Wp.Ctypes.c_object ->
            Wp.Memory.Model.loc -> Wp.Lang.F.term -> Wp.Lang.F.pred list
          val assigned :
            Wp.Memory.Model.sigma Wp.Memory.sequence ->
            Wp.Ctypes.c_object ->
            Wp.Memory.Model.loc Wp.Memory.sloc -> Wp.Lang.F.pred list
          val is_null : Wp.Memory.Model.loc -> Wp.Lang.F.pred
          val loc_eq :
            Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred
          val loc_lt :
            Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred
          val loc_neq :
            Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred
          val loc_leq :
            Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.pred
          val loc_diff :
            Wp.Ctypes.c_object ->
            Wp.Memory.Model.loc -> Wp.Memory.Model.loc -> Wp.Lang.F.term
          val valid :
            Wp.Memory.Model.sigma ->
            Wp.Memory.acs -> Wp.Memory.Model.segment -> Wp.Lang.F.pred
          val scope :
            Wp.Memory.Model.sigma ->
            Wp.Mcfg.scope ->
            Cil_types.varinfo list ->
            Wp.Memory.Model.sigma * Wp.Lang.F.pred list
          val global :
            Wp.Memory.Model.sigma -> Wp.Lang.F.term -> Wp.Lang.F.pred
          val included :
            Wp.Memory.Model.segment ->
            Wp.Memory.Model.segment -> Wp.Lang.F.pred
          val separated :
            Wp.Memory.Model.segment ->
            Wp.Memory.Model.segment -> Wp.Lang.F.pred
        end
    end
  module Cint :
    sig
      val of_real : Wp.Ctypes.c_int -> Wp.Lang.F.unop
      val iconvert : Wp.Ctypes.c_int -> Wp.Lang.F.unop
      val irange : Wp.Ctypes.c_int -> Wp.Lang.F.term -> Wp.Lang.F.pred
      val to_cint : Wp.Lang.lfun -> Wp.Ctypes.c_int
      val is_cint : Wp.Lang.lfun -> Wp.Ctypes.c_int
      type model = NoRange | Natural | Machine
      val configure : Wp.Cint.model -> unit
      val iopp : Wp.Ctypes.c_int -> Wp.Lang.F.unop
      val iadd : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val isub : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val imul : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val idiv : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val imod : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val bnot : Wp.Ctypes.c_int -> Wp.Lang.F.unop
      val band : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val bxor : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val bor : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val blsl : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val blsr : Wp.Ctypes.c_int -> Wp.Lang.F.binop
      val l_not : Wp.Lang.F.unop
      val l_and : Wp.Lang.F.binop
      val l_xor : Wp.Lang.F.binop
      val l_or : Wp.Lang.F.binop
      val l_lsl : Wp.Lang.F.binop
      val l_lsr : Wp.Lang.F.binop
      val f_lnot : Wp.Lang.lfun
      val f_land : Wp.Lang.lfun
      val f_lxor : Wp.Lang.lfun
      val f_lor : Wp.Lang.lfun
      val f_lsl : Wp.Lang.lfun
      val f_lsr : Wp.Lang.lfun
      val f_bit : Wp.Lang.lfun
      val is_cint_simplifier : Wp.Conditions.simplifier
      val is_positive_or_null : Wp.Lang.F.term -> bool
    end
  module Cfloat :
    sig
      type model = Real | Float
      val configure : Wp.Cfloat.model -> unit
      val code_lit : float -> Wp.Lang.F.term
      val acsl_lit : Cil_types.logic_real -> Wp.Lang.F.term
      val real_of_int : Wp.Lang.F.unop
      val float_of_int : Wp.Ctypes.c_float -> Wp.Lang.F.unop
      val fconvert : Wp.Ctypes.c_float -> Wp.Lang.F.unop
      val frange : Wp.Ctypes.c_float -> Wp.Lang.F.term -> Wp.Lang.F.pred
      val fopp : Wp.Ctypes.c_float -> Wp.Lang.F.unop
      val fadd : Wp.Ctypes.c_float -> Wp.Lang.F.binop
      val fsub : Wp.Ctypes.c_float -> Wp.Lang.F.binop
      val fmul : Wp.Ctypes.c_float -> Wp.Lang.F.binop
      val fdiv : Wp.Ctypes.c_float -> Wp.Lang.F.binop
      val f_iabs : Wp.Lang.lfun
      val f_rabs : Wp.Lang.lfun
      val f_sqrt : Wp.Lang.lfun
      val f_model : Wp.Lang.lfun
      val f_delta : Wp.Lang.lfun
      val f_epsilon : Wp.Lang.lfun
      val flt_rnd : Wp.Ctypes.c_float -> Wp.Lang.lfun
      val flt_add : Wp.Ctypes.c_float -> Wp.Lang.lfun
      val flt_mul : Wp.Ctypes.c_float -> Wp.Lang.lfun
      val flt_div : Wp.Ctypes.c_float -> Wp.Lang.lfun
      val flt_sqrt : Wp.Ctypes.c_float -> Wp.Lang.lfun
    end
  module Sigma :
    sig
      module Make :
        functor
          (C : Memory.Chunk) (H : sig
                                    type t = C.t
                                    type set
                                    type 'a 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->
          sig
            type chunk = C.t
            type domain = H.set
            type t
            val create : unit -> t
            val copy : t -> t
            val merge : t -> t -> t * Passive.t * Passive.t
            val join : t -> t -> Passive.t
            val assigned : t -> t -> domain -> Lang.F.pred Bag.t
            val mem : t -> chunk -> bool
            val get : t -> chunk -> Lang.F.var
            val value : t -> chunk -> Lang.F.term
            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 : t -> domain -> t
            val havoc_chunk : t -> chunk -> t
            val havoc_any : call:bool -> t -> t
            val domain : t -> domain
            val pretty : Format.formatter -> t -> unit
          end
    end
  module CodeSemantics :
    sig
      module Make :
        functor (M : Memory.Model->
          sig
            type loc = M.loc
            type value = Wp.CodeSemantics.Make.loc Wp.Memory.value
            type sigma = M.Sigma.t
            val cval : Wp.CodeSemantics.Make.value -> Wp.Lang.F.term
            val cloc :
              Wp.CodeSemantics.Make.value -> Wp.CodeSemantics.Make.loc
            val cast :
              Cil_types.typ ->
              Cil_types.typ ->
              Wp.CodeSemantics.Make.value -> Wp.CodeSemantics.Make.value
            val equal_typ :
              Cil_types.typ ->
              Wp.CodeSemantics.Make.value ->
              Wp.CodeSemantics.Make.value -> Wp.Lang.F.pred
            val equal_obj :
              Wp.Ctypes.c_object ->
              Wp.CodeSemantics.Make.value ->
              Wp.CodeSemantics.Make.value -> Wp.Lang.F.pred
            val exp :
              Wp.CodeSemantics.Make.sigma ->
              Cil_types.exp -> Wp.CodeSemantics.Make.value
            val cond :
              Wp.CodeSemantics.Make.sigma -> Cil_types.exp -> Wp.Lang.F.pred
            val lval :
              Wp.CodeSemantics.Make.sigma ->
              Cil_types.lval -> Wp.CodeSemantics.Make.loc
            val call :
              Wp.CodeSemantics.Make.sigma ->
              Cil_types.exp -> Wp.CodeSemantics.Make.loc
            val loc_of_exp :
              Wp.CodeSemantics.Make.sigma ->
              Cil_types.exp -> Wp.CodeSemantics.Make.loc
            val val_of_exp :
              Wp.CodeSemantics.Make.sigma -> Cil_types.exp -> Wp.Lang.F.term
            val return :
              Wp.CodeSemantics.Make.sigma ->
              Cil_types.typ -> Cil_types.exp -> Wp.Lang.F.term
            val is_zero :
              Wp.CodeSemantics.Make.sigma ->
              Wp.Ctypes.c_object ->
              Wp.CodeSemantics.Make.loc -> Wp.Lang.F.pred
            val is_exp_range :
              Wp.CodeSemantics.Make.sigma ->
              Wp.CodeSemantics.Make.loc ->
              Wp.Ctypes.c_object ->
              Wp.Lang.F.term ->
              Wp.Lang.F.term ->
              Wp.CodeSemantics.Make.value option -> Wp.Lang.F.pred
            val instance_of :
              Wp.CodeSemantics.Make.loc ->
              Cil_types.kernel_function -> Wp.Lang.F.pred
          end
    end
  module LogicCompiler :
    sig
      type polarity = [ `Negative | `NoPolarity | `Positive ]
      module Make :
        functor (M : Memory.Model->
          sig
            type value = M.loc Wp.Memory.value
            type logic = M.loc Wp.Memory.logic
            type sigma = M.Sigma.t
            type chunk = M.Chunk.t
            type call
            type frame
            val pp_frame :
              Format.formatter -> Wp.LogicCompiler.Make.frame -> unit
            val frame :
              Cil_types.kernel_function -> Wp.LogicCompiler.Make.frame
            val call :
              Cil_types.kernel_function ->
              Wp.LogicCompiler.Make.value list -> Wp.LogicCompiler.Make.call
            val call_pre :
              Wp.LogicCompiler.Make.sigma ->
              Wp.LogicCompiler.Make.call ->
              Wp.LogicCompiler.Make.sigma -> Wp.LogicCompiler.Make.frame
            val call_post :
              Wp.LogicCompiler.Make.sigma ->
              Wp.LogicCompiler.Make.call ->
              Wp.LogicCompiler.Make.sigma Wp.Memory.sequence ->
              Wp.LogicCompiler.Make.frame
            val formal :
              Cil_types.varinfo -> Wp.LogicCompiler.Make.value option
            val return : unit -> Cil_types.typ
            val result : unit -> Wp.Lang.F.var
            val status : unit -> Wp.Lang.F.var
            val trigger : Wp.Definitions.trigger -> unit
            val guards : Wp.LogicCompiler.Make.frame -> Wp.Lang.F.pred list
            val mem_frame : Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma
            val mem_at_frame :
              Wp.LogicCompiler.Make.frame ->
              Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma
            val in_frame :
              Wp.LogicCompiler.Make.frame -> ('-> 'b) -> '-> 'b
            val get_frame : unit -> Wp.LogicCompiler.Make.frame
            type env
            val new_env :
              Cil_datatype.Logic_var.t list -> Wp.LogicCompiler.Make.env
            val move :
              Wp.LogicCompiler.Make.env ->
              Wp.LogicCompiler.Make.sigma -> Wp.LogicCompiler.Make.env
            val sigma :
              Wp.LogicCompiler.Make.env -> Wp.LogicCompiler.Make.sigma
            val env_at :
              Wp.LogicCompiler.Make.env ->
              Wp.Clabels.c_label -> Wp.LogicCompiler.Make.env
            val mem_at :
              Wp.LogicCompiler.Make.env ->
              Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma
            val env_let :
              Wp.LogicCompiler.Make.env ->
              Cil_types.logic_var ->
              Wp.LogicCompiler.Make.logic -> Wp.LogicCompiler.Make.env
            val env_letp :
              Wp.LogicCompiler.Make.env ->
              Cil_types.logic_var ->
              Wp.Lang.F.pred -> Wp.LogicCompiler.Make.env
            val env_letval :
              Wp.LogicCompiler.Make.env ->
              Cil_types.logic_var ->
              Wp.LogicCompiler.Make.value -> Wp.LogicCompiler.Make.env
            val term :
              Wp.LogicCompiler.Make.env -> Cil_types.term -> Wp.Lang.F.term
            val pred :
              Wp.LogicCompiler.polarity ->
              Wp.LogicCompiler.Make.env ->
              Cil_types.predicate Cil_types.named -> Wp.Lang.F.pred
            val logic :
              Wp.LogicCompiler.Make.env ->
              Cil_types.term -> Wp.LogicCompiler.Make.logic
            val region :
              Wp.LogicCompiler.Make.env ->
              Cil_types.term -> M.loc Wp.Memory.sloc list
            val bootstrap_term :
              (Wp.LogicCompiler.Make.env -> Cil_types.term -> Wp.Lang.F.term) ->
              unit
            val bootstrap_pred :
              (Wp.LogicCompiler.polarity ->
               Wp.LogicCompiler.Make.env ->
               Cil_types.predicate Cil_types.named -> Wp.Lang.F.pred) ->
              unit
            val bootstrap_logic :
              (Wp.LogicCompiler.Make.env ->
               Cil_types.term -> Wp.LogicCompiler.Make.logic) ->
              unit
            val bootstrap_region :
              (Wp.LogicCompiler.Make.env ->
               Cil_types.term -> M.loc Wp.Memory.sloc list) ->
              unit
            val call_fun :
              Wp.LogicCompiler.Make.env ->
              Cil_types.logic_info ->
              (Cil_types.logic_label * Cil_types.logic_label) list ->
              Wp.Lang.F.term list -> Wp.Lang.F.term
            val call_pred :
              Wp.LogicCompiler.Make.env ->
              Cil_types.logic_info ->
              (Cil_types.logic_label * Cil_types.logic_label) list ->
              Wp.Lang.F.term list -> Wp.Lang.F.pred
            val logic_var :
              Wp.LogicCompiler.Make.env ->
              Cil_types.logic_var -> Wp.LogicCompiler.Make.logic
            val logic_info :
              Wp.LogicCompiler.Make.env ->
              Cil_types.logic_info -> Wp.Lang.F.pred option
            val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
          end
    end
  module LogicSemantics :
    sig
      type polarity = [ `Negative | `NoPolarity | `Positive ]
      module Make :
        functor (M : Memory.Model->
          sig
            type loc = M.loc
            type sigma = M.Sigma.t
            type value = M.loc Wp.Memory.value
            type logic = M.loc Wp.Memory.logic
            type region = M.loc Wp.Memory.sloc list
            val pp_logic :
              Format.formatter -> Wp.LogicSemantics.Make.logic -> unit
            val pp_sloc :
              Format.formatter ->
              Wp.LogicSemantics.Make.loc Wp.Memory.sloc -> unit
            val pp_region :
              Format.formatter -> Wp.LogicSemantics.Make.region -> unit
            type call
            type frame
            val pp_frame :
              Format.formatter -> Wp.LogicSemantics.Make.frame -> unit
            val get_frame : unit -> Wp.LogicSemantics.Make.frame
            val in_frame :
              Wp.LogicSemantics.Make.frame -> ('-> 'b) -> '-> 'b
            val mem_frame :
              Wp.Clabels.c_label -> Wp.LogicSemantics.Make.sigma
            val mem_at_frame :
              Wp.LogicSemantics.Make.frame ->
              Wp.Clabels.c_label -> Wp.LogicSemantics.Make.sigma
            val call :
              Cil_types.kernel_function ->
              Wp.LogicSemantics.Make.value list ->
              Wp.LogicSemantics.Make.call
            val frame :
              Cil_types.kernel_function -> Wp.LogicSemantics.Make.frame
            val call_pre :
              Wp.LogicSemantics.Make.sigma ->
              Wp.LogicSemantics.Make.call ->
              Wp.LogicSemantics.Make.sigma -> Wp.LogicSemantics.Make.frame
            val call_post :
              Wp.LogicSemantics.Make.sigma ->
              Wp.LogicSemantics.Make.call ->
              Wp.LogicSemantics.Make.sigma Wp.Memory.sequence ->
              Wp.LogicSemantics.Make.frame
            val return : unit -> Cil_types.typ
            val result : unit -> Wp.Lang.F.var
            val status : unit -> Wp.Lang.F.var
            val guards : Wp.LogicSemantics.Make.frame -> Wp.Lang.F.pred list
            type env
            val new_env :
              Cil_types.logic_var list -> Wp.LogicSemantics.Make.env
            val move :
              Wp.LogicSemantics.Make.env ->
              Wp.LogicSemantics.Make.sigma -> Wp.LogicSemantics.Make.env
            val sigma :
              Wp.LogicSemantics.Make.env -> Wp.LogicSemantics.Make.sigma
            val mem_at :
              Wp.LogicSemantics.Make.env ->
              Wp.Clabels.c_label -> Wp.LogicSemantics.Make.sigma
            val call_env :
              Wp.LogicSemantics.Make.sigma -> Wp.LogicSemantics.Make.env
            val term :
              Wp.LogicSemantics.Make.env -> Cil_types.term -> Wp.Lang.F.term
            val pred :
              Wp.LogicSemantics.polarity ->
              Wp.LogicSemantics.Make.env ->
              Cil_types.predicate Cil_types.named -> Wp.Lang.F.pred
            val region :
              Wp.LogicSemantics.Make.env ->
              Cil_types.term -> Wp.LogicSemantics.Make.region
            val assigns :
              Wp.LogicSemantics.Make.env ->
              Cil_types.identified_term Cil_types.assigns ->
              (Wp.Ctypes.c_object * Wp.LogicSemantics.Make.region) list
              option
            val assigns_from :
              Wp.LogicSemantics.Make.env ->
              Cil_types.identified_term Cil_types.from list ->
              (Wp.Ctypes.c_object * Wp.LogicSemantics.Make.region) list
            val val_of_term :
              Wp.LogicSemantics.Make.env -> Cil_types.term -> Wp.Lang.F.term
            val loc_of_term :
              Wp.LogicSemantics.Make.env ->
              Cil_types.term -> Wp.LogicSemantics.Make.loc
            val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
            val vars : Wp.LogicSemantics.Make.region -> Wp.Lang.F.Vars.t
            val occurs :
              Wp.Lang.F.var -> Wp.LogicSemantics.Make.region -> bool
            val valid :
              Wp.LogicSemantics.Make.sigma ->
              Wp.Memory.acs ->
              Wp.Ctypes.c_object ->
              Wp.LogicSemantics.Make.region -> Wp.Lang.F.pred
            val included :
              Wp.Ctypes.c_object ->
              Wp.LogicSemantics.Make.region ->
              Wp.Ctypes.c_object ->
              Wp.LogicSemantics.Make.region -> Wp.Lang.F.pred
            val separated :
              (Wp.Ctypes.c_object * Wp.LogicSemantics.Make.region) list ->
              Wp.Lang.F.pred
          end
    end
  module MemVar :
    sig
      type param = NotUsed | ByValue | ByRef | InContext | InHeap
      module type VarUsage =
        sig
          val datatype : string
          val param : Cil_types.varinfo -> Wp.MemVar.param
          val separation : unit -> Wp.Separation.clause
        end
      module Make : functor (V : VarUsage) (M : Memory.Model-> Memory.Model
    end
  module MemTyped :
    sig
      val configure : Model.tuning
      val datatype : string
      val separation : unit -> Separation.clause list
      module Chunk : Memory.Chunk
      module Heap :
        sig
          type t = Chunk.t
          type set
          type 'a 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 Sigma :
        sig
          type chunk = Chunk.t
          type domain = Heap.set
          type t
          val create : unit -> t
          val copy : t -> t
          val merge : t -> t -> t * Passive.t * Passive.t
          val join : t -> t -> Passive.t
          val assigned : t -> t -> domain -> Lang.F.pred Bag.t
          val mem : t -> chunk -> bool
          val get : t -> chunk -> Lang.F.var
          val value : t -> chunk -> Lang.F.term
          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 : t -> domain -> t
          val havoc_chunk : t -> chunk -> t
          val havoc_any : call:bool -> t -> t
          val domain : t -> domain
          val pretty : Format.formatter -> t -> unit
        end
      type loc
      type chunk = Chunk.t
      type sigma = Sigma.t
      type segment = loc Memory.rloc
      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 block_length : sigma -> Ctypes.c_object -> loc -> Lang.F.term
      val cast : Ctypes.c_object Memory.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 -> Heap.set
      val load : sigma -> Ctypes.c_object -> loc -> loc Memory.value
      val copied :
        sigma Memory.sequence ->
        Ctypes.c_object -> loc -> loc -> Lang.F.pred list
      val stored :
        sigma Memory.sequence ->
        Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.pred list
      val assigned :
        sigma Memory.sequence ->
        Ctypes.c_object -> loc Memory.sloc -> Lang.F.pred 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 -> Memory.acs -> segment -> Lang.F.pred
      val scope :
        sigma ->
        Mcfg.scope -> Cil_types.varinfo list -> sigma * 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
      type pointer = NoCast | Fits | Unsafe
      val pointer : Wp.MemTyped.pointer Wp.Context.value
    end
  module Factory :
    sig
      type mheap = Hoare | ZeroAlias | Typed of Wp.MemTyped.pointer
      type mvar = Raw | Var | Ref | Caveat
      type setup = {
        mvar : Wp.Factory.mvar;
        mheap : Wp.Factory.mheap;
        cint : Wp.Cint.model;
        cfloat : Wp.Cfloat.model;
      }
      type driver = Wp.LogicBuiltins.driver
      val ident : Wp.Factory.setup -> string
      val descr : Wp.Factory.setup -> string
      val memory :
        Wp.Factory.mheap -> Wp.Factory.mvar -> (module Wp.Memory.Model)
      val configure :
        Wp.Factory.setup -> Wp.Factory.driver -> Wp.Model.tuning
      val instance : Wp.Factory.setup -> Wp.Factory.driver -> Wp.Model.t
      val default : Wp.Factory.setup
      val parse :
        ?default:Wp.Factory.setup ->
        ?warning:(string -> unit) -> string list -> Wp.Factory.setup
    end
  module VCS :
    sig
      type prover = Why3 of string | Why3ide | AltErgo | Coq | Qed
      type mode = BatchMode | EditMode | FixMode
      type language = L_why3 | L_coq | L_altergo
      module Pmap :
        sig
          type key = prover
          type +'a 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
      val language_of_prover : Wp.VCS.prover -> Wp.VCS.language
      val language_of_name : string -> Wp.VCS.language option
      val name_of_prover : Wp.VCS.prover -> string
      val filename_for_prover : Wp.VCS.prover -> string
      val prover_of_name : string -> Wp.VCS.prover option
      val language_of_prover_name : string -> Wp.VCS.language option
      val mode_of_prover_name : string -> Wp.VCS.mode
      val name_of_mode : Wp.VCS.mode -> string
      val pp_prover : Format.formatter -> Wp.VCS.prover -> unit
      val pp_language : Format.formatter -> Wp.VCS.language -> unit
      val pp_mode : Format.formatter -> Wp.VCS.mode -> unit
      val cmp_prover : Wp.VCS.prover -> Wp.VCS.prover -> int
      type verdict =
          NoResult
        | Invalid
        | Unknown
        | Timeout
        | Stepout
        | Computing of (unit -> unit)
        | Checked
        | Valid
        | Failed
      type result = {
        verdict : Wp.VCS.verdict;
        solver_time : float;
        prover_time : float;
        prover_steps : int;
        prover_errpos : Lexing.position option;
        prover_errmsg : string;
      }
      val no_result : Wp.VCS.result
      val valid : Wp.VCS.result
      val checked : Wp.VCS.result
      val invalid : Wp.VCS.result
      val unknown : Wp.VCS.result
      val timeout : Wp.VCS.result
      val stepout : Wp.VCS.result
      val computing : (unit -> unit) -> Wp.VCS.result
      val failed : ?pos:Lexing.position -> string -> Wp.VCS.result
      val kfailed :
        ?pos:Lexing.position ->
        ('a, Format.formatter, unit, Wp.VCS.result) Pervasives.format4 -> 'a
      val result :
        ?solver:float ->
        ?time:float -> ?steps:int -> Wp.VCS.verdict -> Wp.VCS.result
      val is_verdict : Wp.VCS.result -> bool
      val pp_result : Format.formatter -> Wp.VCS.result -> unit
      val compare : Wp.VCS.result -> Wp.VCS.result -> int
    end
  module VC :
    sig
      type t
      val get_id : Wp.VC.t -> string
      val get_model : Wp.VC.t -> Wp.Model.t
      val get_description : Wp.VC.t -> string
      val get_property : Wp.VC.t -> Property.t
      val get_result : Wp.VC.t -> Wp.VCS.prover -> Wp.VCS.result
      val get_results : Wp.VC.t -> (Wp.VCS.prover * Wp.VCS.result) list
      val get_logout : Wp.VC.t -> Wp.VCS.prover -> string
      val get_logerr : Wp.VC.t -> Wp.VCS.prover -> string
      val is_trivial : Wp.VC.t -> bool
      val get_formula : Wp.VC.t -> Wp.Lang.F.pred
      val clear : unit -> unit
      val proof : Property.t -> Wp.VC.t list
      val remove : Property.t -> unit
      val iter_ip : (Wp.VC.t -> unit) -> Property.t -> unit
      val iter_kf :
        (Wp.VC.t -> unit) -> ?bhv:string list -> Kernel_function.t -> unit
      val generate_ip : ?model:string -> Property.t -> Wp.VC.t Bag.t
      val generate_kf :
        ?model:string ->
        ?bhv:string list -> Kernel_function.t -> Wp.VC.t Bag.t
      val generate_call : ?model:string -> Cil_types.stmt -> Wp.VC.t Bag.t
      val prove :
        Wp.VC.t ->
        ?mode:Wp.VCS.mode ->
        ?start:(Wp.VC.t -> unit) ->
        ?callin:(Wp.VC.t -> Wp.VCS.prover -> unit) ->
        ?callback:(Wp.VC.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
        Wp.VCS.prover -> bool Task.task
      val spawn :
        Wp.VC.t ->
        ?start:(Wp.VC.t -> unit) ->
        ?callin:(Wp.VC.t -> Wp.VCS.prover -> unit) ->
        ?callback:(Wp.VC.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
        ?success:(Wp.VC.t -> Wp.VCS.prover option -> unit) ->
        (Wp.VCS.mode * Wp.VCS.prover) list -> unit
      val server : ?procs:int -> unit -> Task.server
      val command : Wp.VC.t Bag.t -> unit
    end
end