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

Mainstream installed provers

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

For the command line

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

For scripts

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

val get_memlimit : config -> int

0 means no-memlimit

Results

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

Result that fits the default configuration

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