Frama-C:
Plug-ins:
Libraries:

Frama-C API - Wpo

type index =
  1. | Axiomatic of string option
  2. | 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 = {
  1. po_gid : string;
    (*

    goal identifier

    *)
  2. po_sid : string;
    (*

    goal short identifier (without model)

    *)
  3. po_name : string;
    (*

    goal informal name

    *)
  4. po_idx : index;
    (*

    goal index

    *)
  5. po_model : WpContext.model;
  6. po_pid : WpPropId.prop_id;
  7. po_formula : VC_Annot.t;
}
val get_gid : t -> string
val get_property : t -> Frama_c_kernel.Property.t
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 -> Frama_c_kernel.Filepath.t

only filename, might not exists

val get_file_logerr : t -> VCS.prover -> Frama_c_kernel.Filepath.t

only filename, might not exists

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 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 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
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_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 pp_flow : Stdlib.Format.formatter -> unit

VC Generator interface.

class type generator = object ... end