Module Wp.Wpo

type index =
| Axiomatic of string option
| Function of Frama_c_kernel.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
and 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 : WpContext.model;
po_pid : WpPropId.prop_id;
po_formula : formula;
}
module Index : Stdlib.Map.OrderedType with type t = index
module Gmap : Stdlib.Map.S with type key = index
val get_gid : t -> string

Dynamically exported

  • since Nitrogen-20111001
val get_property : t -> Frama_c_kernel.Property.t

Dynamically exported

  • since Oxygen-20120901
val get_index : t -> index
val get_label : t -> string
val get_model : t -> WpContext.model
val get_scope : t -> WpContext.scope
val get_context : t -> WpContext.context
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 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 add_modified_hook : ( t -> unit ) -> unit

Hook is invoked for each goal results modification. Remark: clear() does not trigger those hooks, Cf. add_cleared_hook instead.

val add_removed_hook : ( t -> unit ) -> unit

Hook is invoked for each removed goal. Remark: clear() does not trigger those hooks, Cf. add_cleared_hook instead.

val add_cleared_hook : ( unit -> unit ) -> unit

Register a hook when the entire table is cleared.

val compute : t -> Definitions.axioms option * Conditions.sequent

Warning: Prover results are stored as they are from prover output, without taking into consideration that validity is inverted for smoke tests.

On the contrary, proof validity is computed with respect to smoke test/non-smoke test.

val has_verdict : t -> VCS.prover -> bool

Definite result for this prover (not computing)

val get_result : t -> VCS.prover -> VCS.result

Raw prover result (without any respect to smoke tests)

val get_results : t -> (VCS.prover * VCS.result) list

All raw prover results (without any respect to smoke tests)

val get_proof : t -> [ `Passed | `Failed | `Unknown ] * Frama_c_kernel.Property.t

Consolidated wrt to associated property and smoke test.

val get_target : t -> Frama_c_kernel.Property.t

Associated property.

val is_trivial : t -> bool

Currently trivial sequent (no forced simplification)

val is_valid : t -> bool

Checks for some prover with valid verdict (no forced simplification)

val all_not_valid : t -> bool

Checks for all provers to give a non-valid, computed verdict

val is_passed : t -> bool

valid, or all-not-valid for smoke tests

val has_unknown : t -> bool

Checks there is some provers with a non-valid verdict

val warnings : t -> Warning.t list
val is_tactic : t -> bool
val is_smoke_test : t -> bool
val iter : ?ip:Frama_c_kernel.Property.t -> ?index:index -> ?on_axiomatics:( string option -> unit ) -> ?on_behavior: ( Frama_c_kernel.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 : Frama_c_kernel.Property.t -> t list

All POs related to a given property. Dynamically exported

  • since Oxygen-20120901
val bar : string
val pp_index : Stdlib.Format.formatter -> index -> unit
val pp_warnings : Stdlib.Format.formatter -> Warning.t list -> unit
val pp_depend : Stdlib.Format.formatter -> Frama_c_kernel.Property.t -> unit
val pp_dependency : Frama_c_kernel.Description.kf -> Stdlib.Format.formatter -> Frama_c_kernel.Property.t -> unit
val pp_dependencies : Frama_c_kernel.Description.kf -> Stdlib.Format.formatter -> Frama_c_kernel.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 -> Frama_c_kernel.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.

VC Generator interface.

class type generator = object ... end