package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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_Lemma : sig ... end
Sourcemodule VC_Annot : sig ... end

Proof Obligations

Sourcetype formula =
  1. | GoalLemma of VC_Lemma.t
  2. | GoalAnnot of VC_Annot.t
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 : formula;
}
Sourcemodule Index : Map.OrderedType with type t = index
Sourcemodule Gmap : Map.S with type key = index
Sourceval get_gid : t -> string

Dynamically exported

  • since Nitrogen-20111001
Sourceval get_property : t -> Frama_c_kernel.Property.t

Dynamically exported

  • since Oxygen-20120901
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 -> string

only filename, might not exists

Sourceval get_file_logerr : t -> VCS.prover -> string

only filename, might not exists

Sourceval get_files : t -> (string * string) list
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.

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

Dynamically exported.

  • since Nitrogen-20111001
Sourceval goals_of_property : Frama_c_kernel.Property.t -> t list

All POs related to a given property. Dynamically exported

  • since Oxygen-20120901
Sourceval bar : string
Sourceval pp_index : Format.formatter -> index -> unit
Sourceval pp_warnings : Format.formatter -> Warning.t list -> unit
Sourceval pp_goal : Format.formatter -> t -> unit
Sourceval pp_title : Format.formatter -> t -> unit
Sourceval pp_logfile : Format.formatter -> t -> VCS.prover -> 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 prover_of_name : string -> VCS.prover option

Dynamically exported.

VC Generator interface.

Sourceclass type generator = object ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct