sig
type index =
Axiomatic of string option
| Function of Cil_types.kernel_function * string option
module DISK :
sig
val cache_log :
pid:Wp.WpPropId.prop_id ->
model:Wp.Model.t ->
prover:Wp.VCS.prover -> result:Wp.VCS.result -> string
val pretty :
pid:Wp.WpPropId.prop_id ->
model:Wp.Model.t ->
prover:Wp.VCS.prover ->
result:Wp.VCS.result -> Format.formatter -> unit
val file_kf :
kf:Cil_types.kernel_function ->
model:Wp.Model.t -> prover:Wp.VCS.prover -> string
val file_goal :
pid:Wp.WpPropId.prop_id ->
model:Wp.Model.t -> prover:Wp.VCS.prover -> string
val file_logout :
pid:Wp.WpPropId.prop_id ->
model:Wp.Model.t -> prover:Wp.VCS.prover -> string
val file_logerr :
pid:Wp.WpPropId.prop_id ->
model:Wp.Model.t -> prover:Wp.VCS.prover -> string
end
module GOAL :
sig
type t
val dummy : Wp.Wpo.GOAL.t
val trivial : Wp.Wpo.GOAL.t
val is_trivial : Wp.Wpo.GOAL.t -> bool
val make : Wp.Conditions.sequent -> Wp.Wpo.GOAL.t
val compute_proof : Wp.Wpo.GOAL.t -> Wp.Lang.F.pred
val compute_descr : Wp.Wpo.GOAL.t -> Wp.Conditions.sequent
val get_descr : Wp.Wpo.GOAL.t -> Wp.Conditions.sequent
val compute : Wp.Wpo.GOAL.t -> unit
val qed_time : Wp.Wpo.GOAL.t -> float
end
module VC_Lemma :
sig
type t = {
lemma : Wp.Definitions.dlemma;
depends : Wp.LogicUsage.logic_lemma list;
mutable sequent : Wp.Conditions.sequent option;
}
val is_trivial : Wp.Wpo.VC_Lemma.t -> bool
val cache_descr :
Wp.Wpo.VC_Lemma.t -> (Wp.VCS.prover * Wp.VCS.result) list -> string
end
module VC_Annot :
sig
type t = {
axioms : Wp.Definitions.axioms option;
goal : Wp.Wpo.GOAL.t;
tags : Wp.Splitter.tag list;
warn : Wp.Warning.t list;
deps : Property.Set.t;
path : Cil_datatype.Stmt.Set.t;
effect : (Cil_types.stmt * Wp.WpPropId.effect_source) option;
}
val resolve : Wp.Wpo.VC_Annot.t -> bool
val is_trivial : Wp.Wpo.VC_Annot.t -> bool
val cache_descr :
pid:Wp.WpPropId.prop_id ->
Wp.Wpo.VC_Annot.t -> (Wp.VCS.prover * Wp.VCS.result) list -> string
end
module VC_Check :
sig
type t = {
qed : Wp.Lang.F.term;
raw : Wp.Lang.F.term;
goal : Wp.Lang.F.pred;
}
end
type formula =
GoalLemma of Wp.Wpo.VC_Lemma.t
| GoalAnnot of Wp.Wpo.VC_Annot.t
| GoalCheck of Wp.Wpo.VC_Check.t
type po = Wp.Wpo.t
and t = {
po_gid : string;
po_sid : string;
po_name : string;
po_idx : Wp.Wpo.index;
po_model : Wp.Model.t;
po_pid : Wp.WpPropId.prop_id;
po_formula : Wp.Wpo.formula;
}
module S :
sig
type t = po
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
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 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 find : elt -> t -> elt
val of_list : elt list -> t
val min_elt : t -> elt
val max_elt : t -> elt
val split : elt -> t -> t * bool * t
val nearest_elt_le : elt -> t -> elt
val nearest_elt_ge : elt -> t -> elt
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module 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 find_opt : key -> 'a t -> 'a option
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
module Key :
sig
type t = key
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 Make :
functor (Data : Datatype.S) ->
sig
type t = Data.t t
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
end
module Hashtbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted :
?cmp:(key -> key -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted_by_entry :
cmp:(key * 'a -> key * 'a -> int) ->
(key -> 'a -> unit) -> 'a t -> unit
val fold_sorted_by_entry :
cmp:(key * 'a -> key * 'a -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted_by_value :
cmp:('a -> 'a -> int) -> (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted_by_value :
cmp:('a -> 'a -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val find_opt : 'a t -> key -> 'a option
val find_def : 'a t -> key -> 'a -> 'a
val memo : 'a t -> key -> (key -> 'a) -> 'a
val structural_descr : Structural_descr.t -> Structural_descr.t
val make_type : 'a Type.t -> 'a t Type.t
module Key :
sig
type t = key
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 Make :
functor (Data : Datatype.S) ->
sig
type t = Data.t t
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
end
end
module Index : sig type t = index val compare : t -> t -> int end
module Gmap :
sig
type key = index
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 find_opt : key -> 'a t -> 'a option
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
end
val get_gid : Wp.Wpo.t -> string
val get_property : Wp.Wpo.t -> Property.t
val get_index : Wp.Wpo.t -> Wp.Wpo.index
val get_label : Wp.Wpo.t -> string
val get_model : Wp.Wpo.t -> Wp.Model.t
val get_model_id : Wp.Wpo.t -> string
val get_model_name : Wp.Wpo.t -> string
val get_file_logout : Wp.Wpo.t -> Wp.VCS.prover -> string
val get_file_logerr : Wp.Wpo.t -> Wp.VCS.prover -> string
val get_files : Wp.Wpo.t -> (string * string) list
val qed_time : Wp.Wpo.t -> float
val clear : unit -> unit
val remove : Wp.Wpo.t -> unit
val on_remove : (Wp.Wpo.t -> unit) -> unit
val add : Wp.Wpo.t -> unit
val age : Wp.Wpo.t -> int
val resolve : Wp.Wpo.t -> bool
val set_result : Wp.Wpo.t -> Wp.VCS.prover -> Wp.VCS.result -> unit
val clear_results : Wp.Wpo.t -> unit
val compute :
Wp.Wpo.t -> Wp.Definitions.axioms option * Wp.Conditions.sequent
val has_verdict : Wp.Wpo.t -> Wp.VCS.prover -> bool
val get_result : Wp.Wpo.t -> Wp.VCS.prover -> Wp.VCS.result
val get_results : Wp.Wpo.t -> (Wp.VCS.prover * Wp.VCS.result) list
val get_proof : Wp.Wpo.t -> bool * Property.t
val is_trivial : Wp.Wpo.t -> bool
val is_proved : Wp.Wpo.t -> bool
val is_unknown : Wp.Wpo.t -> bool
val warnings : Wp.Wpo.t -> Wp.Warning.t list
val is_valid : Wp.VCS.result -> bool
val get_time : Wp.VCS.result -> float
val get_steps : Wp.VCS.result -> int
val is_check : Wp.Wpo.t -> bool
val is_tactic : Wp.Wpo.t -> bool
val iter :
?ip:Property.t ->
?index:Wp.Wpo.index ->
?on_axiomatics:(string option -> unit) ->
?on_behavior:(Cil_types.kernel_function -> string option -> unit) ->
?on_goal:(Wp.Wpo.t -> unit) -> unit -> unit
val iter_on_goals : (Wp.Wpo.t -> unit) -> unit
val goals_of_property : Property.t -> Wp.Wpo.t list
val bar : string
val kf_context : Wp.Wpo.index -> Description.kf
val pp_index : Format.formatter -> Wp.Wpo.index -> unit
val pp_warnings : Format.formatter -> Wp.Warning.t list -> unit
val pp_depend : Format.formatter -> Property.t -> unit
val pp_dependency :
Description.kf -> Format.formatter -> Property.t -> unit
val pp_dependencies :
Description.kf -> Format.formatter -> Property.t list -> unit
val pp_goal : Format.formatter -> Wp.Wpo.t -> unit
val pp_title : Format.formatter -> Wp.Wpo.t -> unit
val pp_logfile : Format.formatter -> Wp.Wpo.t -> Wp.VCS.prover -> unit
val pp_axiomatics : Format.formatter -> string option -> unit
val pp_function :
Format.formatter -> Kernel_function.t -> string option -> unit
val pp_goal_flow : Format.formatter -> Wp.Wpo.t -> unit
val prover_of_name : string -> Wp.VCS.prover option
end