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.WpContext.model ->
prover:Wp.VCS.prover -> result:Wp.VCS.result -> string
val pretty :
pid:Wp.WpPropId.prop_id ->
model:Wp.WpContext.model ->
prover:Wp.VCS.prover ->
result:Wp.VCS.result -> Stdlib.Format.formatter -> unit
val file_kf :
kf:Cil_types.kernel_function ->
model:Wp.WpContext.model -> prover:Wp.VCS.prover -> string
val file_goal :
pid:Wp.WpPropId.prop_id ->
model:Wp.WpContext.model -> prover:Wp.VCS.prover -> string
val file_logout :
pid:Wp.WpPropId.prop_id ->
model:Wp.WpContext.model -> prover:Wp.VCS.prover -> string
val file_logerr :
pid:Wp.WpPropId.prop_id ->
model:Wp.WpContext.model -> 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 : pid:Wp.WpPropId.prop_id -> Wp.Wpo.GOAL.t -> unit
val compute_proof :
pid:Wp.WpPropId.prop_id -> Wp.Wpo.GOAL.t -> Wp.Lang.F.pred
val compute_descr :
pid:Wp.WpPropId.prop_id -> Wp.Wpo.GOAL.t -> Wp.Conditions.sequent
val get_descr : Wp.Wpo.GOAL.t -> Wp.Conditions.sequent
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 is_trivial : Wp.Wpo.VC_Annot.t -> bool
val resolve : pid:Wp.WpPropId.prop_id -> 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
type formula =
GoalLemma of Wp.Wpo.VC_Lemma.t
| GoalAnnot of Wp.Wpo.VC_Annot.t
type po = Wp.Wpo.t
and t = {
po_gid : string;
po_leg : string;
po_sid : string;
po_name : string;
po_idx : Wp.Wpo.index;
po_model : Wp.WpContext.model;
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 disjoint : t -> t -> bool
val diff : t -> t -> t
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val map : (elt -> elt) -> t -> t
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 filter_map : (elt -> elt option) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val min_elt_opt : t -> elt option
val max_elt : t -> elt
val max_elt_opt : t -> elt option
val choose : t -> elt
val choose_opt : t -> elt option
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val find_opt : elt -> t -> elt option
val find_first : (elt -> bool) -> t -> elt
val find_first_opt : (elt -> bool) -> t -> elt option
val find_last : (elt -> bool) -> t -> elt
val find_last_opt : (elt -> bool) -> t -> elt option
val of_list : elt list -> t
val to_seq_from : elt -> t -> elt Seq.t
val to_seq : t -> elt Seq.t
val add_seq : elt Seq.t -> t -> t
val of_seq : elt Seq.t -> 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 update : key -> ('a option -> 'a option) -> '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 union : (key -> 'a -> 'a -> 'a option) -> 'a t -> '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 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 filter_map : (key -> 'a -> 'b option) -> 'a t -> 'b 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 min_binding_opt : 'a t -> (key * 'a) option
val max_binding : 'a t -> key * 'a
val max_binding_opt : 'a t -> (key * 'a) option
val choose : 'a t -> key * 'a
val choose_opt : 'a t -> (key * 'a) option
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 find_first : (key -> bool) -> 'a t -> key * 'a
val find_first_opt : (key -> bool) -> 'a t -> (key * 'a) option
val find_last : (key -> bool) -> 'a t -> key * 'a
val find_last_opt : (key -> bool) -> 'a t -> (key * 'a) option
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val to_seq : 'a t -> (key * 'a) Seq.t
val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
val of_seq : (key * 'a) Seq.t -> 'a 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 to_seq : 'a t -> (key * 'a) Seq.t
val to_seq_keys : 'a t -> key Seq.t
val to_seq_values : 'a t -> 'a Seq.t
val add_seq : 'a t -> (key * 'a) Seq.t -> unit
val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
val of_seq : (key * 'a) Seq.t -> 'a t
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 update : key -> ('a option -> 'a option) -> '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 union : (key -> 'a -> 'a -> 'a option) -> 'a t -> '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 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 filter_map : (key -> 'a -> 'b option) -> 'a t -> 'b 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 min_binding_opt : 'a t -> (key * 'a) option
val max_binding : 'a t -> key * 'a
val max_binding_opt : 'a t -> (key * 'a) option
val choose : 'a t -> key * 'a
val choose_opt : 'a t -> (key * 'a) option
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 find_first : (key -> bool) -> 'a t -> key * 'a
val find_first_opt : (key -> bool) -> 'a t -> (key * 'a) option
val find_last : (key -> bool) -> 'a t -> key * 'a
val find_last_opt : (key -> bool) -> 'a t -> (key * 'a) option
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val to_seq : 'a t -> (key * 'a) Seq.t
val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
val of_seq : (key * 'a) Seq.t -> 'a 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.WpContext.model
val get_scope : Wp.Wpo.t -> Wp.WpContext.scope
val get_context : Wp.Wpo.t -> Wp.WpContext.context
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 reduce : Wp.Wpo.t -> bool
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 -> [ `Failed | `Passed | `Unknown ] * Property.t
val get_target : Wp.Wpo.t -> Property.t
val is_trivial : Wp.Wpo.t -> bool
val is_proved : Wp.Wpo.t -> bool
val is_unknown : Wp.Wpo.t -> bool
val is_passed : 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_tactic : Wp.Wpo.t -> bool
val is_smoke_test : 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 : Stdlib.Format.formatter -> Wp.Wpo.index -> unit
val pp_warnings : Stdlib.Format.formatter -> Wp.Warning.t list -> unit
val pp_depend : Stdlib.Format.formatter -> Property.t -> unit
val pp_dependency :
Description.kf -> Stdlib.Format.formatter -> Property.t -> unit
val pp_dependencies :
Description.kf -> Stdlib.Format.formatter -> Property.t list -> unit
val pp_goal : Stdlib.Format.formatter -> Wp.Wpo.t -> unit
val pp_title : Stdlib.Format.formatter -> Wp.Wpo.t -> unit
val pp_logfile :
Stdlib.Format.formatter -> Wp.Wpo.t -> Wp.VCS.prover -> unit
val pp_axiomatics : Stdlib.Format.formatter -> string option -> unit
val pp_function :
Stdlib.Format.formatter -> Kernel_function.t -> string option -> unit
val pp_goal_flow : Stdlib.Format.formatter -> Wp.Wpo.t -> unit
val prover_of_name : string -> Wp.VCS.prover option
class type generator =
object
method compute_call : Cil_types.stmt -> Wp.Wpo.t Bag.t
method compute_ip : Property.t -> Wp.Wpo.t Bag.t
method compute_main :
?fct:Wp.Wp_parameters.functions ->
?bhv:string list -> ?prop:string list -> unit -> Wp.Wpo.t Bag.t
method model : Wp.WpContext.model
end
end