module Wpo:sig
..end
type
index =
| |
Axiomatic of |
| |
Function of |
module DISK:sig
..end
module GOAL:sig
..end
module VC_Lemma:sig
..end
module VC_Annot:sig
..end
module VC_Check:sig
..end
type
formula =
| |
GoalLemma of |
| |
GoalAnnot of |
| |
GoalCheck of |
typepo =
t
type
t = {
|
po_gid : |
(* | goal identifier | *) |
|
po_sid : |
(* | goal short identifier (without model) | *) |
|
po_name : |
(* | goal informal name | *) |
|
po_idx : |
(* | goal index | *) |
|
po_model : |
|||
|
po_pid : |
|||
|
po_formula : |
module S:Datatype.S_with_collections
with type t = po
module Index:Map.OrderedType
with type t = index
module Gmap:FCMap.S
with type key = index
val get_gid : t -> string
Dynamically exported
val get_property : t -> Property.t
Dynamically exported
val get_index : t -> index
val get_label : t -> string
val get_model : t -> Wp.Model.t
val get_model_id : t -> string
val get_model_name : t -> string
val get_file_logout : t -> Wp.VCS.prover -> string
only filename, might not exists
val get_file_logerr : t -> Wp.VCS.prover -> string
only filename, might not exists
val get_files : t -> (string * string) list
val qed_time : t -> float
val clear : unit -> unit
val remove : t -> unit
val on_remove : (t -> unit) -> unit
val add : t -> unit
val age : t -> int
val resolve : t -> bool
tries simplification
val set_result : t -> Wp.VCS.prover -> Wp.VCS.result -> unit
val clear_results : t -> unit
val compute : t -> Wp.Definitions.axioms option * Wp.Conditions.sequent
val has_verdict : t -> Wp.VCS.prover -> bool
val get_result : t -> Wp.VCS.prover -> Wp.VCS.result
val get_results : t -> (Wp.VCS.prover * Wp.VCS.result) list
val get_proof : t -> bool * Property.t
val is_trivial : t -> bool
do not tries simplification, do not check prover results
val is_proved : t -> bool
do not tries simplification, check prover results
val is_unknown : t -> bool
val warnings : t -> Wp.Warning.t list
val is_valid : Wp.VCS.result -> bool
true
if the result is valid. Dynamically exported.
val get_time : Wp.VCS.result -> float
val get_steps : Wp.VCS.result -> int
val is_check : t -> bool
val is_tactic : t -> bool
val iter : ?ip:Property.t ->
?index:index ->
?on_axiomatics:(string option -> unit) ->
?on_behavior:(Cil_types.kernel_function -> string option -> unit) ->
?on_goal:(t -> unit) -> unit -> unit
val iter_on_goals : (t -> unit) -> unit
Dynamically exported.
val goals_of_property : Property.t -> t list
All POs related to a given property. Dynamically exported
val bar : string
val kf_context : index -> Description.kf
val pp_index : Format.formatter -> 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 -> t -> unit
val pp_title : Format.formatter -> t -> unit
val pp_logfile : Format.formatter -> 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 -> t -> unit
val prover_of_name : string -> Wp.VCS.prover option
Dynamically exported.