package frama-c

  1. Overview
  2. Docs
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.