Module Wp.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

Proof Obligations

type formula = 
| GoalLemma of VC_Lemma.t
| GoalAnnot of VC_Annot.t
type po = t 
type t = {
   po_gid : string; (*

goal identifier

*)
   po_sid : string; (*

goal short identifier (without model)

*)
   po_name : string; (*

goal informal name

*)
   po_idx : index; (*

goal index

*)
   po_model : Wp.WpContext.model;
   po_pid : Wp.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: Map.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.WpContext.model
val get_scope : t -> Wp.WpContext.scope
val get_context : t -> Wp.WpContext.context
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 reduce : t -> bool

tries simplification

val resolve : t -> bool

tries simplification and set result if valid

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 -> [ `Failed | `Passed | `Unknown ] * Property.t
val get_target : t -> 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

at least one prover returns « Unknown »

val is_passed : t -> bool

proved, or unknown for smoke tests

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_tactic : t -> bool
val is_smoke_test : 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 -> Wp.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 -> Wp.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 -> Wp.VCS.prover option

Dynamically exported.

VC Generator interface.

class type generator = object .. end