Frama-C API - 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_Annot : sig ... end
Proof Obligations
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 : VC_Annot.t;
}
module S : Frama_c_kernel.Datatype.S_with_collections with type t = po
val get_gid : t -> string
val get_property : t -> Frama_c_kernel.Property.t
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 -> Frama_c_kernel.Filepath.Normalized.t
only filename, might not exists
val get_file_logerr : t -> VCS.prover -> Frama_c_kernel.Filepath.Normalized.t
only filename, might not exists
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 modified : t -> unit
val computed : t -> bool
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
Return all results (without any respect to smoke tests).
val get_prover_results : t -> (VCS.prover * VCS.result) list
Return all 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_fully_valid : t -> bool
Checks for some prover or script with valid verdict (no forced qed)
val is_locally_valid : t -> bool
Checks for some prover (no tactic) with valid verdict (no forced qed)
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
val goals_of_property : Frama_c_kernel.Property.t -> t list
val pp_index : Stdlib.Format.formatter -> index -> unit
val pp_goal : Stdlib.Format.formatter -> t -> unit
val pp_title : Stdlib.Format.formatter -> t -> 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
VC Generator interface.
class type generator = object ... end