Module LogicBuiltins.W

module W: 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