Module Wp.ProverSource

Provers configuration and information

Prover

Sourcetype 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
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval pretty : Format.formatter -> t -> unit
Sourceval ident : t -> string

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

Sourceval name : t -> string

Name of the prover, typically CVC5

Sourceval shortcut : t -> string

Shortcut name (typically lowercase name)

Sourceval version : t -> string

Frama-C version for TIP and Qed

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

Prover list

Sourceval 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
Sourceval add_reload_hook : (unit -> unit) -> unit
Sourceval enabled : t -> bool
Sourceval set_prover : t -> state:bool -> unit
Sourceval add_prover_update_hook : (t -> unit) -> unit
Sourceval use_scripts : unit -> bool
Sourceval use_strategies : unit -> bool
Sourceval set_use_scripts : bool -> unit

Note: if false, also disables strategies

Sourceval set_use_strategies : bool -> unit

Note: if true, also enables scripts

Sourceval add_scripts_update_hook : (unit -> unit) -> unit

Interactive provers configuration

Sourcemodule InteractiveMode : sig ... end

TIP configuration

Sourcemodule TipMode : sig ... end