package frama-c

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

Module Wp.VCSSource

Provers and Proof Obligations Results

Verification Condition Status

Prover

Sourcetype prover =
  1. | Why3 of Why3Provers.t
    (*

    Prover via WHY

    *)
  2. | Qed
    (*

    Qed Solver

    *)
  3. | Tactical
    (*

    Interactive Prover

    *)
Sourcetype mode =
  1. | Batch
    (*

    Only check scripts

    *)
  2. | Update
    (*

    Check and update scripts

    *)
  3. | Edit
    (*

    Edit then check scripts

    *)
  4. | Fix
    (*

    Try check script, then edit script on non-success

    *)
  5. | FixUpdate
    (*

    Update & Fix

    *)
Sourcemodule Pset : Set.S with type elt = prover
Sourcemodule Pmap : Map.S with type key = prover
Sourceval name_of_prover : prover -> string
Sourceval title_of_prover : ?version:bool -> prover -> string
Sourceval filename_for_prover : prover -> string
Sourceval title_of_mode : mode -> string
Sourceval parse_mode : string -> mode
Sourceval parse_prover : string -> prover option
Sourceval pp_prover : Format.formatter -> prover -> unit
Sourceval pp_mode : Format.formatter -> mode -> unit
Sourceval cmp_prover : prover -> prover -> int

Config

None means current WP option default. Some 0 means prover default.

Sourcetype config = {
  1. valid : bool;
  2. timeout : float option;
  3. stepout : int option;
}
Sourceval current : unit -> config

Current parameters

Sourceval default : config

all None

Sourceval get_timeout : ?kf:Frama_c_kernel.Kernel_function.t -> smoke:bool -> config -> float

0.0 means no-timeout

Sourceval get_stepout : config -> int

0 means no-stepout

Results

Sourcetype verdict =
  1. | NoResult
  2. | Invalid
  3. | Unknown
  4. | Timeout
  5. | Stepout
  6. | Computing of unit -> unit
  7. | Valid
  8. | Failed
Sourcetype result = {
  1. verdict : verdict;
  2. cached : bool;
  3. solver_time : float;
  4. prover_time : float;
  5. prover_steps : int;
  6. prover_errpos : Lexing.position option;
  7. prover_errmsg : string;
}
Sourceval no_result : result
Sourceval valid : result
Sourceval invalid : result
Sourceval unknown : result
Sourceval stepout : int -> result
Sourceval timeout : float -> result
Sourceval computing : (unit -> unit) -> result
Sourceval failed : ?pos:Lexing.position -> string -> result
Sourceval kfailed : ?pos:Lexing.position -> ('a, Format.formatter, unit, result) format4 -> 'a
Sourceval cached : result -> result

only for true verdicts

Sourceval result : ?cached:bool -> ?solver:float -> ?time:float -> ?steps:int -> verdict -> result
Sourceval is_auto : prover -> bool
Sourceval is_result : verdict -> bool
Sourceval is_verdict : result -> bool
Sourceval is_valid : result -> bool
Sourceval is_trivial : result -> bool
Sourceval is_not_valid : result -> bool
Sourceval is_computing : result -> bool
Sourceval is_proved : smoke:bool -> result -> bool
Sourceval smoked : verdict -> verdict
Sourceval verdict : smoke:bool -> result -> verdict
Sourceval configure : result -> config
Sourceval autofit : result -> bool

Result that fits the default configuration

Sourceval name_of_verdict : verdict -> string
Sourceval pp_result : Format.formatter -> result -> unit
Sourceval pp_result_qualif : ?updating:bool -> prover -> result -> Format.formatter -> unit
Sourceval compare : result -> result -> int
Sourceval combine : verdict -> verdict -> verdict
Sourceval merge : result -> result -> result
Sourceval leq : result -> result -> bool
Sourceval choose : result -> result -> result
Sourceval best : result list -> result
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