Module Whyconf

module Whyconf: sig .. end
Managing the configuration of Why3


General configuration


type config 
A configuration linked to an rc file. Whyconf gives access to every sections of the rc file (Whyconf.get_section, Whyconf.set_section, Whyconf.get_family, Whyconf.set_family) but the section main and the family prover which are dealt by it (Whyconf.get_main, Whyconf.set_main, Whyconf.get_provers, Whyconf.set_provers
exception ConfigFailure of string * string
exception DuplicateShortcut of string
val read_config : string option -> config
read_config conf_file :
val merge_config : config -> string -> config
merge_config config filename merge the content of filename into config
val save_config : config -> unit
save_config config save the configuration
val default_config : string -> config
default_config filename create a default configuration which is going to be saved in filename
val get_conf_file : config -> string
get_conf_file config get the rc file corresponding to this configuration
type main 

Main section


val get_main : config -> main
get_main config get the main section stored in the Rc file
val set_main : config -> main -> config
set_main config main replace the main section by the given one
val libdir : main -> string
val datadir : main -> string
val loadpath : main -> string list
val timelimit : main -> int
val memlimit : main -> int
val running_provers_max : main -> int
val cntexample : main -> bool
val set_limits : main -> int -> int -> int -> main
val set_cntexample : main -> bool -> main
val plugins : main -> string list
val pluginsdir : main -> string
val set_plugins : main -> string list -> main
val add_plugin : main -> string -> main
val load_plugins : main -> unit

Provers



Prover's identifier


type prover = {
   prover_name : string;
   prover_version : string;
   prover_altern : string;
}
record of necessary data for a given external prover
val print_prover : Format.formatter -> prover -> unit
val print_prover_parseable_format : Format.formatter -> prover -> unit
val prover_parseable_format : prover -> string
module Prover: OrderedHashedType  with type t = prover
Printer for prover
module Mprover: Extmap.S  with type key = prover
module Sprover: Extset.S  with module M = Mprover
module Hprover: Exthtbl.S  with type key = prover

Prover configuration


type config_prover = {
   prover : prover;
   command : string;
   command_steps : string option;
   driver : string;
   in_place : bool;
   editor : string;
   interactive : bool;
   extra_options : string list;
   extra_drivers : string list;
}
val get_complete_command : config_prover -> with_steps:bool -> string
add the extra_options to the command
val get_provers : config -> config_prover Mprover.t
get_provers config get the prover family stored in the Rc file. The keys are the unique ids of the prover (argument of the family)
val set_provers : config ->
?shortcuts:prover Stdlib.Mstr.t ->
config_prover Mprover.t -> config
set_provers config provers replace all the family prover by the one given
val is_prover_known : config -> prover -> bool
test if a prover is detected
val get_prover_shortcuts : config -> prover Stdlib.Mstr.t
return the prover shortcuts
val set_prover_shortcuts : config -> prover Stdlib.Mstr.t -> config
set the prover shortcuts
type config_editor = {
   editor_name : string;
   editor_command : string;
   editor_options : string list;
}
module Meditor: Extmap.S  with type key = string
val set_editors : config -> config_editor Meditor.t -> config
replace the set of editors
val get_editors : config -> config_editor Meditor.t
returns the set of editors
val editor_by_id : config -> string -> config_editor
return the configuration of the editor if found, otherwise return Not_found

prover upgrade policy
type prover_upgrade_policy = 
| CPU_keep
| CPU_upgrade of prover
| CPU_duplicate of prover
val set_prover_upgrade_policy : config ->
prover -> prover_upgrade_policy -> config
set_prover_upgrade c p cpu sets or updates the policy to follow if the prover p is absent from the system
val get_prover_upgrade_policy : config -> prover -> prover_upgrade_policy
get_prover_upgrade config returns a map providing the policy to follow for each absent prover (if it has already been decided by the user and thus stored in the config)
val get_policies : config -> prover_upgrade_policy Mprover.t
val set_policies : config ->
prover_upgrade_policy Mprover.t -> config

strategies
type config_strategy = {
   strategy_name : string;
   strategy_desc : string;
   strategy_code : string;
   strategy_shortcut : string;
}
val get_strategies : config -> config_strategy Stdlib.Mstr.t
val add_strategy : config -> config_strategy -> config
type filter_prover 
filter prover
val mk_filter_prover : ?version:string -> ?altern:string -> string -> filter_prover
val print_filter_prover : Format.formatter -> filter_prover -> unit
val parse_filter_prover : string -> filter_prover
parse the string representing a filter_prover: regexp must start with ^. Partial match will be used.
val filter_prover_with_shortcut : config -> filter_prover -> filter_prover
resolve prover shortcut in filter
val filter_prover : filter_prover -> prover -> bool
test if the prover match the filter prover
val filter_provers : config ->
filter_prover -> config_prover Mprover.t
Get all the provers that match this filter
exception ProverNotFound of config * filter_prover
exception ProverAmbiguity of config * filter_prover
* config_prover Mprover.t
exception ParseFilterProver of string
val filter_one_prover : config -> filter_prover -> config_prover
find the uniq prover that verify the filter. If it doesn't exists raise ProverNotFound or raise ProverAmbiguity
val why3_regexp_of_string : string -> Str.regexp

For accesing other parts of the configuration


val get_section : config -> string -> Rc.section option
Access to the Rc.t

get_section config name Same as Rc.get_section except name must not be "main"

val get_family : config -> string -> Rc.family
get_family config name Same as Rc.get_family except name must not be prover
val set_section : config -> string -> Rc.section -> config
set_section config name Same as Rc.set_section except name must not be "main"
val set_family : config -> string -> Rc.family -> config
set_family config name Same as Rc.set_family except name must not be prover

Common command line options
module Args: sig .. end

Loading drivers with relative names
val load_driver : main -> Env.env -> string -> string list -> Driver.driver
wrapper for loading a driver from a file that may be relative to the datadir. See Driver.load_driver_absolute