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 iiter : (Wp.Ctypes.c_int -> unit) -> unit       val fiter : (Wp.Ctypes.c_float -> unit) -> unit       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 is_comp : Wp.Ctypes.c_object -> Cil_types.compinfo -> bool       val is_array : Wp.Ctypes.c_object -> elt:Wp.Ctypes.c_object -> bool       val get_array :         Wp.Ctypes.c_object -> (Wp.Ctypes.c_object * int option) option       val get_array_size : Wp.Ctypes.c_object -> int option       val array_size : Wp.Ctypes.arrayinfo -> int option       val array_dim : Wp.Ctypes.arrayinfo -> Wp.Ctypes.c_object * int       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.predicate       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;         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       val mk_pred_info :         Wp.WpPropId.prop_id -> Cil_types.predicate -> 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       val run_once_for_each_ast :         name:string -> (unit -> unit) -> unit -> unit     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 consequence : term -> term -> term           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           module Check :             sig               val reset : unit -> unit               val set : string -> unit               val is_set : unit -> bool               val iter :                 (qed:term -> raw:term -> goal:Wp.Lang.F.pred -> unit) -> unit             end         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) 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 pretty : Format.formatter -> Wp.Vset.set -> 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         | 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 union :             Wp.Memory.Sigma.domain ->             Wp.Memory.Sigma.domain -> Wp.Memory.Sigma.domain           val empty : 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 union : domain -> domain -> domain               val empty : 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 convert : Wp.Ctypes.c_int -> Wp.Lang.F.unop       val to_cint : Wp.Lang.lfun -> Wp.Ctypes.c_int       val is_cint : Wp.Lang.lfun -> Wp.Ctypes.c_int       type model = Natural | Machine       val configure : Wp.Cint.model -> unit       val current : unit -> Wp.Cint.model       val range : Wp.Ctypes.c_int -> Wp.Lang.F.term -> Wp.Lang.F.pred       val downcast : Wp.Ctypes.c_int -> Wp.Lang.F.unop       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 convert : Wp.Ctypes.c_float -> Wp.Lang.F.unop       val range : 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 union : domain -> domain -> domain             val empty : 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 -> 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 -> 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 -> 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 | InArray | 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 union : domain -> domain -> domain           val empty : 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 union : (key -> '-> '-> 'a option) -> 'a t -> '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 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 stepout : Wp.VCS.result       val timeout : int -> 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