Frama-C:
Plug-ins:
Libraries:

Frama-C API - VCS

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 : Stdlib.Set.S with type elt = prover
module Pmap : Stdlib.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 : Stdlib.Format.formatter -> prover -> unit
val pp_mode : Stdlib.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 : Stdlib.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:Stdlib.Lexing.position -> string -> result
val kfailed : ?pos:Stdlib.Lexing.position -> ('a, Stdlib.Format.formatter, unit, result) Stdlib.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 : Stdlib.Format.formatter -> result -> unit
val pp_model : Stdlib.Format.formatter -> model -> unit
val pp_result_qualif : ?updating:bool -> prover -> result -> Stdlib.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