Module Wpo

module Wpo: sig .. end

Proof Obligations



type index = 
| Axiomatic of string option
| Function of Cil_types.kernel_function * string option

Proof Obligations


module DISK: sig .. end
module GOAL: sig .. end
module VC_Lemma: sig .. end
module VC_Annot: sig .. end
module VC_Check: sig .. end

Proof Obligations


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_sid : string;
   po_name : string;
   po_idx : index;
   po_model : Model.t;
   po_pid : WpPropId.prop_id;
   po_updater : Emitter.t;
   po_formula : 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
Since Nitrogen-20111001
val get_property : t -> Property.t
Dynamically exported
Since Oxygen-20120901
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_file_logout : t -> VCS.prover -> string
only filename, might not exists
val get_file_logerr : t -> VCS.prover -> string
only filename, might not exists
val get_files : t -> (string * string) list
val clear : unit -> unit
val remove : t -> unit
val resolve : t -> bool
val add : t -> unit
val age : t -> int
val set_result : t -> VCS.prover -> VCS.result -> unit
val get_result : t -> VCS.prover -> VCS.result
Dynamically exported.
val get_results : t -> (VCS.prover * VCS.result) list
val get_proof : t -> bool * Property.t
val is_trivial : t -> bool
val warnings : t -> Warning.t list
val is_valid : VCS.result -> 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 is_check : 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.
Since Nitrogen-20111001
val goals_of_property : Property.t -> t list
All POs related to a given property. Dynamically exported
Since Oxygen-20120901
val bar : string
val kf_context : index -> Description.kf
val pp_index : Format.formatter -> index -> unit
val pp_warnings : Format.formatter -> 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 -> 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 -> VCS.prover option
Dynamically exported.