Frama-C:
Plug-ins:
Libraries:

Frama-C API - Why3Env

Why3 (and provers) configuration

Why3 configuration

val why3_version : string
val env : unit -> Why3.Env.env
val config : unit -> Why3.Whyconf.config
val configure : unit -> unit
val set_procs : int -> unit

Prover information

type prover = Why3.Whyconf.prover
val ident_why3 : prover -> string
val ident_wp : prover -> string
val title : ?version:bool -> prover -> string
val name : prover -> string
val version : prover -> string
val compare : prover -> prover -> int
val equal : prover -> prover -> bool
val hash : prover -> int
val lookup : ?fallback:bool -> string -> prover option
val provers : unit -> prover list
val is_auto : prover -> bool
val is_available : prover -> bool
val is_mainstream : prover -> bool
val has_counter_examples : prover -> bool
val with_counter_examples : prover -> prover option
type model = Why3.Model_parser.concrete_syntax_term