module WpLog: 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 |
| |
WP_Fct of |
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
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
print the given file if the debugging category
"print-generated" is set