Module Wpo

module Wpo: sig .. end

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 
type t = {
   po_gid : string; (*

goal identifier

*)
   po_leg : string; (*

legacy goal identifier

*)
   po_sid : string; (*

goal short identifier (without model)

*)
   po_name : string; (*

goal informal name

*)
   po_idx : index; (*

goal index

*)
   po_model : Model.t;
   po_pid : WpPropId.prop_id;
   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

val get_property : t -> Property.t

Dynamically exported

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 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 reduce : t -> bool

tries simplification

val resolve : t -> bool

tries simplification and set result if valid

val set_result : t -> VCS.prover -> VCS.result -> unit
val clear_results : t -> unit
val compute : t -> Definitions.axioms option * Conditions.sequent
val has_verdict : t -> VCS.prover -> bool
val get_result : t -> VCS.prover -> VCS.result
val get_results : t -> (VCS.prover * 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 -> Warning.t list
val is_valid : VCS.result -> bool

true if the result is valid. Dynamically exported.

val get_time : VCS.result -> float
val get_steps : 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 : Stdlib.Format.formatter -> 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 -> t -> unit
val pp_title : Stdlib.Format.formatter -> t -> unit
val pp_logfile : Stdlib.Format.formatter -> 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 -> t -> unit
val prover_of_name : string -> VCS.prover option

Dynamically exported.