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