Module Wp.WpoSource

Sourcetype index =
  1. | Axiomatic of string option
  2. | Function of Frama_c_kernel.Cil_types.kernel_function * string option

Proof Obligations

Sourcemodule DISK : sig ... end
Sourcemodule GOAL : sig ... end
Sourcemodule VC_Annot : sig ... end

Proof Obligations

Sourcetype po = t
Sourceand 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;
}
Sourceval get_gid : t -> string
Sourceval get_property : t -> Frama_c_kernel.Property.t
Sourceval get_index : t -> index
Sourceval get_label : t -> string
Sourceval get_model : t -> WpContext.model
Sourceval get_scope : t -> WpContext.scope
Sourceval get_context : t -> WpContext.context

only filename, might not exists

only filename, might not exists

Sourceval qed_time : t -> float
Sourceval clear : unit -> unit
Sourceval remove : t -> unit
Sourceval add : t -> unit
Sourceval age : t -> int
Sourceval reduce : t -> bool

tries simplification

Sourceval resolve : t -> bool

tries simplification and set result if valid

Sourceval set_result : t -> VCS.prover -> VCS.result -> unit
Sourceval clear_results : t -> unit
Sourceval 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.

Sourceval 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.

Sourceval add_cleared_hook : (unit -> unit) -> unit

Register a hook when the entire table is cleared.

Sourceval modified : t -> unit
Sourceval computed : t -> bool

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.

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

Definite result for this prover (not computing)

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

Raw prover result (without any respect to smoke tests)

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

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

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

Consolidated wrt to associated property and smoke test.

Associated property.

Sourceval is_trivial : t -> bool

Currently trivial sequent (no forced simplification)

Sourceval is_valid : t -> bool

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

Sourceval all_not_valid : t -> bool

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

Sourceval is_passed : t -> bool

valid, or all-not-valid for smoke tests

Sourceval has_unknown : t -> bool

Checks there is some provers with a non-valid verdict

Sourceval warnings : t -> Warning.t list
Sourceval is_tactic : t -> bool
Sourceval is_smoke_test : t -> bool
Sourceval 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
Sourceval iter_on_goals : (t -> unit) -> unit
Sourceval goals_of_property : Frama_c_kernel.Property.t -> t list
Sourceval pp_index : Format.formatter -> index -> unit
Sourceval pp_goal : Format.formatter -> t -> unit
Sourceval pp_title : Format.formatter -> t -> unit
Sourceval pp_axiomatics : Format.formatter -> string option -> unit
Sourceval pp_function : Format.formatter -> Frama_c_kernel.Kernel_function.t -> string option -> unit
Sourceval pp_goal_flow : Format.formatter -> t -> unit
Sourceval pp_flow : Format.formatter -> unit

VC Generator interface.

Sourceclass type generator = object ... end