package frama-c

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

Provers and Proof Obligations Results

Verification Condition Status

Prover

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

    Prover via WHY

    *)
  2. | Qed
    (*

    Qed Solver

    *)
  3. | Tactical
    (*

    Interactive Prover

    *)
type 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

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

Config

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

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

Current parameters

val default : config

all None

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

0.0 means no-timeout

val get_stepout : config -> int

0 means no-stepout

Results

type verdict =
  1. | NoResult
  2. | Invalid
  3. | Unknown
  4. | Timeout
  5. | Stepout
  6. | Computing of unit -> unit
  7. | Valid
  8. | Failed
type 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;
}
val no_result : result
val valid : result
val invalid : result
val unknown : result
val stepout : int -> result
val timeout : float -> result
val computing : (unit -> unit) -> result
val failed : ?pos:Lexing.position -> string -> result
val kfailed : ?pos:Lexing.position -> ('a, Format.formatter, unit, result) format4 -> 'a
val cached : result -> result

only for true verdicts

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

Result that fits the default configuration

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