package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/Wpo/index.html

Module `Wp.Wpo`Source

Sourcetype index =

| Axiomatic of string option
| 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 = {

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

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

Sourceval get_file_logout : t -> VCS.prover -> Frama_c_kernel.Filepath.Normalized.t

only filename, might not exists

Sourceval get_file_logerr : t -> VCS.prover -> Frama_c_kernel.Filepath.Normalized.t

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

Sourceval modified : t -> unit

Sourceval computed : t -> bool

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

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

Return all results (without any respect to smoke tests).

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

Return all prover results (without any respect to smoke tests).

Source

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

Consolidated wrt to associated property and smoke test.

Sourceval get_target : t -> Frama_c_kernel.Property.t

Associated property.

Sourceval is_trivial : t -> bool

Currently trivial sequent (no forced simplification)

Sourceval is_fully_valid : t -> bool

Checks for some prover or script with valid verdict (no forced qed)

Sourceval is_locally_valid : t -> bool

Checks for some prover (no tactic) with valid verdict (no forced qed)

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

Source

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

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

Source

val 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

On This Page

Proof Obligations
Proof Obligations

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/Wpo/index.html

Module Wp.WpoSource

Proof Obligations

Proof Obligations

Module `Wp.Wpo`Source