Module Wpo
module Wpo: sig
.. end
Proof Obligations
type
index =
val bar : string
val flow : bool Pervasives.ref
val pp_index : Format.formatter -> index -> unit
val pp_axiomatics : Format.formatter -> string option -> unit
val pp_function : Format.formatter -> Kernel_function.t -> string option -> unit
val pp_warnings : Format.formatter -> Warning.t list -> unit
val kf_context : index -> [> `Always | `Context of Cil_types.kernel_function ]
val pp_dependency : Description.kf -> Format.formatter -> Property.t -> unit
val pp_dependencies : Description.kf -> Format.formatter -> Property.t list -> unit
val pp_depend : Format.formatter -> Property.t -> unit
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 =
type
po = t
Dynamically exported as "Wpo.po"
type
t = {
}
val get_index : t -> index
val get_label : t -> string
val get_model : t -> Model.t
val get_model_id : t -> string
val get_model_name : t -> string
val get_depend : t -> Property.Set.elt list
val get_file_logout : t -> VCS.prover -> string
only filename, might not exists
val get_file_logerr : t -> VCS.prover -> string
only filename, might not exists
module Index: sig
.. end
module PODatatype: Datatype.Make_with_collections
(
sig
end
)
module ProverType: Datatype.Make
(
sig
end
)
module ResultType: Datatype.Make
(
sig
end
)
val get_gid : PODatatype.t -> string
Dynamically exported
Since Nitrogen-20111001
val get_property : PODatatype.t -> Property.t
Dynamically exported
Since Oxygen-20120901
val is_check : t -> bool
val is_verdict : VCS.result -> bool
true
if the result is meaningfull (Valid, Unknown or Timeout)
module Hproof: Hashtbl.Make
(
Datatype.Pair
(
Datatype.String
)
(
Property
)
)
module Results: sig
.. end
module WPOset: PODatatype.Set
module WPOmap: PODatatype.Map
module Gmap: FCMap.Make
(
Index
)
module Fmap: Kernel_function.Map
module Pmap: Property.Map
val index_wpo : ('a -> WPOset.t -> 'b -> 'c) ->
('a -> 'b -> WPOset.t) -> 'a -> WPOset.elt -> 'b -> 'c
val unindex_wpo : ('a -> WPOset.t -> 'b -> 'b) ->
('a -> 'b -> WPOset.t) -> 'a -> WPOset.elt -> 'b -> 'b
type
system = {
|
mutable wpo_idx : WPOset.t Gmap.t ; |
|
mutable wpo_kf : WPOset.t Fmap.t ; |
|
mutable wpo_ip : WPOset.t Pmap.t ; |
|
mutable age : int WPOmap.t ; |
|
mutable results : Results.t WPOmap.t ; |
|
proofs : WpAnnot.proof Hproof.t ; |
}
val create_system : unit -> system
val clear_system : system -> unit
module SYSTEM: State_builder.Ref
(
Datatype.Make
(
sig
end
)
)
(
sig
val name : string
val dependencies : State.t list
val default : unit -> Wpo.system
end
)
val clear : unit -> unit
val gid : model:string -> propid:WpPropId.prop_id -> string
val added : int Pervasives.ref
val age : WPOmap.key -> int
val current_age : int Pervasives.ref
val add : WPOmap.key -> unit
val remove : WPOset.elt -> unit
val warnings : t -> Warning.t list
val is_valid : ResultType.t -> bool
true
if the result is valid. Dynamically exported.
Since Nitrogen-20111001
val get_time : VCS.result -> float
val get_steps : VCS.result -> int
val get_proof : t -> bool * Property.t
val update_property_status : t -> VCS.result -> unit
val set_result : WPOmap.key -> Results.Pmap.key -> VCS.result -> unit
val get_result : PODatatype.t -> ProverType.t -> ResultType.t
Dynamically exported.
val is_trivial : t -> bool
val resolve : t -> bool
val get_result : PODatatype.t -> ProverType.t -> ResultType.t
Dynamically exported.
val is_valid : ResultType.t -> bool
true
if the result is valid. Dynamically exported.
Since Nitrogen-20111001
val get_results : WPOmap.key -> (Results.Pmap.key * VCS.result) list
val pp_title : Format.formatter -> t -> unit
val pp_goal : Format.formatter -> WPOmap.key -> unit
val pp_goal_flow : Format.formatter -> WPOmap.key -> unit
type
part =
val iter : ?ip:Pmap.key ->
?index:Gmap.key ->
?on_axiomatics:(string option -> unit) ->
?on_behavior:(Cil_types.kernel_function -> string option -> unit) ->
?on_goal:(WPOset.elt -> unit) -> unit -> unit
val iter_on_goals : (WPOset.elt -> unit) -> unit
Dynamically exported.
Since Nitrogen-20111001
val goals_of_property : Property.t -> PODatatype.t list
All POs related to a given property.
Dynamically exported
Since Oxygen-20120901
val goals_of_property : Property.t -> PODatatype.t list
All POs related to a given property.
Dynamically exported
Since Oxygen-20120901
val prover_of_name : string -> ProverType.t option
Dynamically exported.
val get_model : t -> Model.t
val get_logfile : t -> VCS.prover -> VCS.result -> string
val pp_logfile : Format.formatter -> PODatatype.t -> ProverType.t -> unit
val is_computing : VCS.verdict -> bool
val get_files : WPOmap.key -> (string * string) list
module S: PODatatype