Module VarUsage.WpMain

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: String_set(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: String_list(sig
val option_name : string
val arg_name : string
val help : string
end)

module SkipFunctions: String_list(sig
val option_name : string
val arg_name : string
val help : string
end)

module Behaviors: String_list(sig
val option_name : string
val arg_name : string
val help : string
end)

module Properties: String_list(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: String_list(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 Init: False(sig
val option_name : string
val help : string
end)

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: String_list(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: String_list(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: String_list(sig
val option_name : string
val arg_name : string
val help : string
end)

module CoqLibs: String_list(sig
val option_name : string
val arg_name : string
val help : string
end)

module WhyLibs: String_list(sig
val option_name : string
val arg_name : string
val help : string
end)

module WhyFlags: String_list(sig
val option_name : string
val arg_name : string
val help : string
end)

module AltErgoLibs: String_list(sig
val option_name : string
val arg_name : string
val help : string
end)

module AltErgoFlags: String_list(sig
val option_name : string
val arg_name : string
val help : string
end)

val wp_po : Cmdline.Group.t

module TruncPropIdFileName: Int(sig
val option_name : string
val default : int
val arg_name : string
val help : string
end)

module Print: Action(sig
val option_name : string
val help : string
end)

module Report: String_list(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

val cat_print_generated : Log.category

val print_generated : string -> unit

Debugging Categories

print the given file if the debugging category "print-generated" is set