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 provers : unit -> prover list

Mainstream installed provers

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

For the command line

Sourceval prover_of_name : ?fallback:bool -> string -> prover option

For scripts

Sourceval pp_prover : Format.formatter -> prover -> unit
Sourceval pp_mode : Format.formatter -> mode -> unit
Sourceval eq_prover : prover -> prover -> bool
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;
  4. memlimit : 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

Sourceval get_memlimit : config -> int

0 means no-memlimit

Results

Sourcetype verdict =
  1. | NoResult
  2. | Unknown
  3. | Timeout
  4. | Stepout
  5. | Computing of unit -> unit
  6. | Valid
  7. | Invalid
  8. | Failed
Sourcetype model
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;
  8. prover_model : model;
}
Sourceval no_result : result
Sourceval valid : 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 : ?model:model -> ?cached:bool -> ?solver:float -> ?time:float -> ?steps:int -> verdict -> result
Sourceval is_auto : prover -> bool
Sourceval has_counter_examples : prover -> bool
Sourceval is_prover : prover -> bool
Sourceval is_extern : prover -> bool
Sourceval is_result : verdict -> bool
Sourceval is_proved : smoke:bool -> verdict -> bool
Sourceval is_none : result -> 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 has_model : result -> bool
Sourceval configure : result -> config
Sourceval autofit : result -> bool

Result that fits the default configuration

Sourceval name_of_verdict : ?computing:bool -> verdict -> string
Sourceval pp_result : Format.formatter -> result -> unit
Sourceval pp_model : Format.formatter -> model -> unit
Sourceval pp_result_qualif : ?updating:bool -> prover -> result -> Format.formatter -> unit
Sourceval conjunction : verdict -> verdict -> verdict
Sourceval compare : result -> result -> int
Sourceval best : (prover * result) list -> prover * 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