Module Wpo

module Wpo: sig .. end

Proof Obligations



type index = 
| Axiomatic of string option
| Function of Cil_types.kernel_function * string option
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 = 
| GoalLemma of VC_Lemma.t
| GoalAnnot of VC_Annot.t
| GoalCheck of VC_Check.t
type po = t 
Dynamically exported as "Wpo.po"
type t = {
   po_gid : string;
   po_name : string;
   po_idx : index;
   po_model : Model.t;
   po_pid : WpPropId.prop_id;
   po_updater : Emitter.t;
   po_formula : formula;
}
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
type t = Wpo.po 
include Datatype.Undefined
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val name : string
val reprs : t list
end)
module ProverType: Datatype.Make(sig
type t = VCS.prover 
include Datatype.Undefined
val name : string
val reprs : VCS.prover list
end)
module ResultType: Datatype.Make(sig
type t = VCS.result 
include Datatype.Undefined
val name : string
val reprs : VCS.result list
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
include Datatype.Undefined
type t = Wpo.system 
val name : string
val reprs : Wpo.system list
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
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 -> VCS.prover -> 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 -> (VCS.prover * 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 = 
| Pnone
| Paxiomatic of string option
| Pbehavior of Cil_types.kernel_function * string option
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