Frama-C:
Plug-ins:
Libraries:

Frama-C API - Prover

Provers configuration and information

Prover

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

    Prover via Why3

    *)
  2. | Qed
    (*

    Qed Solver

    *)
  3. | Tactical
    (*

    Interactive Prover

    *)
  4. | CFG
    (*

    Used for properties proved only using CFG. It cannot be disabled/manually enabled.

    *)
module Pset : Frama_c_kernel.Set.S with type elt = t
module Pmap : Frama_c_kernel.Map.S with type key = t
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Stdlib.Format.formatter -> t -> unit
val ident : t -> string

Identifier of the Prover for WP, typically "CVC5:1.2.1"

val name : t -> string

Name of the prover, typically CVC5

val shortcut : t -> string

Shortcut name (typically lowercase name)

val version : t -> string

Frama-C version for TIP and Qed

val title : ?version:bool -> t -> string
val parse : string -> t option
val is_auto : t -> bool
val is_tactical : t -> bool
val is_extern : t -> bool
val has_counter_examples : t -> bool
val filename_for : t -> string
val of_name : ?fallback:bool -> string -> t option

Prover list

val provers : ?filter:(t -> bool) -> unit -> t list

Returns *all* provers that satisfy filter (which defaults _ -> true) E.g. if you need only enabled solvers, it should be called with the enabled function.

  • since 33.0-Arsenic
val add_reload_hook : (unit -> unit) -> unit
val enabled : t -> bool
val set_prover : t -> state:bool -> unit
val add_prover_update_hook : (t -> unit) -> unit
val use_scripts : unit -> bool
val use_strategies : unit -> bool
val set_use_scripts : bool -> unit

Note: if false, also disables strategies

val set_use_strategies : bool -> unit

Note: if true, also enables scripts

val add_scripts_update_hook : (unit -> unit) -> unit

Interactive provers configuration

module InteractiveMode : sig ... end

TIP configuration

module TipMode : sig ... end
val dkey_shell : Wp_parameters.category