sig
type index =
Axiomatic of string option
| Function of Cil_types.kernel_function * string option
module DISK :
sig
val cache_log :
pid:WpPropId.prop_id ->
model:Model.t -> prover:VCS.prover -> result:VCS.result -> string
val pretty :
pid:WpPropId.prop_id ->
model:Model.t ->
prover:VCS.prover ->
result:VCS.result -> Stdlib.Format.formatter -> unit
val file_kf :
kf:Cil_types.kernel_function ->
model:Model.t -> prover:VCS.prover -> string
val file_goal :
pid:WpPropId.prop_id -> model:Model.t -> prover:VCS.prover -> string
val file_logout :
pid:WpPropId.prop_id -> model:Model.t -> prover:VCS.prover -> string
val file_logerr :
pid:WpPropId.prop_id -> model:Model.t -> prover:VCS.prover -> string
end
module GOAL :
sig
type t
val dummy : Wpo.GOAL.t
val trivial : Wpo.GOAL.t
val is_trivial : Wpo.GOAL.t -> bool
val make : Conditions.sequent -> Wpo.GOAL.t
val compute_proof : Wpo.GOAL.t -> Lang.F.pred
val compute_descr : Wpo.GOAL.t -> Conditions.sequent
val get_descr : Wpo.GOAL.t -> Conditions.sequent
val compute : Wpo.GOAL.t -> unit
val qed_time : Wpo.GOAL.t -> float
end
module VC_Lemma :
sig
type t = {
lemma : Definitions.dlemma;
depends : LogicUsage.logic_lemma list;
mutable sequent : Conditions.sequent option;
}
val is_trivial : Wpo.VC_Lemma.t -> bool
val cache_descr :
Wpo.VC_Lemma.t -> (VCS.prover * VCS.result) list -> string
end
module VC_Annot :
sig
type t = {
axioms : Definitions.axioms option;
goal : Wpo.GOAL.t;
tags : Splitter.tag list;
warn : Warning.t list;
deps : Property.Set.t;
path : Cil_datatype.Stmt.Set.t;
effect : (Cil_types.stmt * WpPropId.effect_source) option;
}
val resolve : Wpo.VC_Annot.t -> bool
val is_trivial : Wpo.VC_Annot.t -> bool
val cache_descr :
pid:WpPropId.prop_id ->
Wpo.VC_Annot.t -> (VCS.prover * VCS.result) list -> string
end
module VC_Check :
sig
type t = { qed : Lang.F.term; raw : Lang.F.term; goal : Lang.F.pred; }
end
type formula =
GoalLemma of Wpo.VC_Lemma.t
| GoalAnnot of Wpo.VC_Annot.t
| GoalCheck of Wpo.VC_Check.t
type po = Wpo.t
and t = {
po_gid : string;
po_leg : string;
po_sid : string;
po_name : string;
po_idx : Wpo.index;
po_model : Model.t;
po_pid : WpPropId.prop_id;
po_formula : 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 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 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 : Wpo.t -> string
val get_property : Wpo.t -> Property.t
val get_index : Wpo.t -> Wpo.index
val get_label : Wpo.t -> string
val get_model : Wpo.t -> Model.t
val get_model_id : Wpo.t -> string
val get_model_name : Wpo.t -> string
val get_file_logout : Wpo.t -> VCS.prover -> string
val get_file_logerr : Wpo.t -> VCS.prover -> string
val get_files : Wpo.t -> (string * string) list
val qed_time : Wpo.t -> float
val clear : unit -> unit
val remove : Wpo.t -> unit
val on_remove : (Wpo.t -> unit) -> unit
val add : Wpo.t -> unit
val age : Wpo.t -> int
val reduce : Wpo.t -> bool
val resolve : Wpo.t -> bool
val set_result : Wpo.t -> VCS.prover -> VCS.result -> unit
val clear_results : Wpo.t -> unit
val compute : Wpo.t -> Definitions.axioms option * Conditions.sequent
val has_verdict : Wpo.t -> VCS.prover -> bool
val get_result : Wpo.t -> VCS.prover -> VCS.result
val get_results : Wpo.t -> (VCS.prover * VCS.result) list
val get_proof : Wpo.t -> bool * Property.t
val is_trivial : Wpo.t -> bool
val is_proved : Wpo.t -> bool
val is_unknown : Wpo.t -> bool
val warnings : Wpo.t -> Warning.t list
val is_valid : VCS.result -> bool
val get_time : VCS.result -> float
val get_steps : VCS.result -> int
val is_check : Wpo.t -> bool
val is_tactic : Wpo.t -> bool
val iter :
?ip:Property.t ->
?index:Wpo.index ->
?on_axiomatics:(string option -> unit) ->
?on_behavior:(Cil_types.kernel_function -> string option -> unit) ->
?on_goal:(Wpo.t -> unit) -> unit -> unit
val iter_on_goals : (Wpo.t -> unit) -> unit
val goals_of_property : Property.t -> Wpo.t list
val bar : string
val kf_context : Wpo.index -> Description.kf
val pp_index : Stdlib.Format.formatter -> Wpo.index -> unit
val pp_warnings : Stdlib.Format.formatter -> 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 -> Wpo.t -> unit
val pp_title : Stdlib.Format.formatter -> Wpo.t -> unit
val pp_logfile : Stdlib.Format.formatter -> Wpo.t -> 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 -> Wpo.t -> unit
val prover_of_name : string -> VCS.prover option
end