Wp.Wpo
type index =
| Axiomatic of string option |
| Function of Frama_c_kernel.Cil_types.kernel_function * string option |
module DISK : sig ... end
module GOAL : sig ... end
module VC_Lemma : sig ... end
module VC_Annot : sig ... end
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 S : Frama_c_kernel.Datatype.S_with_collections with type t = po
val get_gid : t -> string
Dynamically exported
val get_property : t -> Frama_c_kernel.Property.t
Dynamically exported
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 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 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 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.
val goals_of_property : Frama_c_kernel.Property.t -> t list
All POs related to a given property. Dynamically exported
val kf_context : index -> Frama_c_kernel.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 -> 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_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