module WpMain: Wp_parameters
module Fc_config: Config
module STRING: String
include struct ... end
val warning : ?current:bool ->
?source:Lexing.position ->
?emitwith:(Log.event -> unit) ->
?echo:bool ->
?once:bool ->
?append:(Format.formatter -> unit) ->
('a, Format.formatter, unit) Pervasives.format -> 'a
val resetdemon : (unit -> unit) list Pervasives.ref
val on_reset : (unit -> unit) -> unit
val reset : unit -> unit
module Log: StringSet
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
val has_dkey : Datatype.String.Set.elt -> bool
val wp_generation : Cmdline.Group.t
module WP: Action
(
sig
val option_name : string
val help : string
end
)
module Functions: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module SkipFunctions: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module Behaviors: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module Properties: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
type
job =
| |
WP_None |
| |
WP_All |
| |
WP_SkipFct of string list |
| |
WP_Fct of string list |
val job : unit -> job
module StatusAll: False
(
sig
val option_name : string
val help : string
end
)
module StatusTrue: False
(
sig
val option_name : string
val help : string
end
)
module StatusFalse: False
(
sig
val option_name : string
val help : string
end
)
module StatusMaybe: True
(
sig
val option_name : string
val help : string
end
)
val wp_model : Cmdline.Group.t
module Model: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module ExternArrays: False
(
sig
val option_name : string
val help : string
end
)
module ExtEqual: False
(
sig
val option_name : string
val help : string
end
)
module Literals: False
(
sig
val option_name : string
val help : string
end
)
val wp_strategy : Cmdline.Group.t
module RTE: False
(
sig
val option_name : string
val help : string
end
)
module Simpl: True
(
sig
val option_name : string
val help : string
end
)
module Let: True
(
sig
val option_name : string
val help : string
end
)
module Prune: True
(
sig
val option_name : string
val help : string
end
)
module Clean: True
(
sig
val option_name : string
val help : string
end
)
module Bits: True
(
sig
val option_name : string
val help : string
end
)
module QedChecks: False
(
sig
val option_name : string
val help : string
end
)
module Split: False
(
sig
val option_name : string
val help : string
end
)
module Invariants: False
(
sig
val option_name : string
val help : string
end
)
module DynCall: False
(
sig
val option_name : string
val help : string
end
)
val wp_prover : Cmdline.Group.t
module Provers: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module Generate: False
(
sig
val option_name : string
val help : string
end
)
module Detect: Action
(
sig
val option_name : string
val help : string
end
)
module Drivers: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module Depth: Int
(
sig
val option_name : string
val default : int
val arg_name : string
val help : string
end
)
module Steps: Int
(
sig
val option_name : string
val default : int
val arg_name : string
val help : string
end
)
module Timeout: Int
(
sig
val option_name : string
val default : int
val arg_name : string
val help : string
end
)
module CoqTimeout: Int
(
sig
val option_name : string
val default : int
val arg_name : string
val help : string
end
)
module Procs: Int
(
sig
val option_name : string
val arg_name : string
val default : int
val help : string
end
)
module ProofTrace: False
(
sig
val option_name : string
val help : string
end
)
val wp_proverlibs : Cmdline.Group.t
module Script: String
(
sig
val option_name : string
val arg_name : string
val default : string
val help : string
end
)
module UpdateScript: True
(
sig
val option_name : string
val help : string
end
)
module CoqTactic: String
(
sig
val option_name : string
val arg_name : string
val default : string
val help : string
end
)
module TryHints: False
(
sig
val option_name : string
val help : string
end
)
module Hints: Int
(
sig
val option_name : string
val arg_name : string
val default : int
val help : string
end
)
module Includes: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module CoqLibs: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module WhyLibs: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module WhyFlags: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module AltErgoLibs: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module AltErgoFlags: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
val wp_po : Cmdline.Group.t
module Print: Action
(
sig
val option_name : string
val help : string
end
)
module Report: StringList
(
sig
val option_name : string
val arg_name : string
val help : string
end
)
module ReportName: String
(
sig
val option_name : string
val arg_name : string
val default : string
val help : string
end
)
module OutputDir: String
(
sig
val option_name : string
val arg_name : string
val default : string
val help : string
end
)
module Check: Action
(
sig
val option_name : string
val help : string
end
)
val wpcheck_provers : unit -> [> `Altergo | `Coq | `Why3 ] list
val dkey : Log.category
val get_env : ?default:string -> string -> string
val dkey : Log.category
val is_out : unit -> bool
val make_output_dir : string -> unit
val unique_tmp : OutputDir.t option Pervasives.ref
val make_tmp_dir : unit -> OutputDir.t
val make_gui_dir : unit -> OutputDir.t
val base_output : unit -> OutputDir.t
call the construction of the directory only once
val base_output : unit -> OutputDir.t
val get_output : unit -> OutputDir.t
val get_output_dir : string -> string
val get_includes : unit -> string list