sig   val verbose_atleast : int -> bool   val debug_atleast : int -> bool   val printf :     ?level:int ->     ?dkey:Log.category ->     ?current:bool ->     ?source:Lexing.position ->     ?append:(Format.formatter -> unit) ->     ?header:(Format.formatter -> unit) ->     ?prefix:string ->     ?suffix:string -> ('a, Format.formatter, unit) format -> 'a   val result : ?level:int -> ?dkey:Log.category -> 'Log.pretty_printer   val feedback :     ?ontty:Log.ontty ->     ?level:int -> ?dkey:Log.category -> 'Log.pretty_printer   val debug : ?level:int -> ?dkey:Log.category -> 'Log.pretty_printer   val warning : 'Log.pretty_printer   val error : 'Log.pretty_printer   val abort : ('a, 'b) Log.pretty_aborter   val failure : 'Log.pretty_printer   val fatal : ('a, 'b) Log.pretty_aborter   val verify : bool -> ('a, bool) Log.pretty_aborter   val not_yet_implemented : ('a, Format.formatter, unit, 'b) format4 -> 'a   val deprecated : string -> now:string -> ('-> 'b) -> '-> 'b   val with_result : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter   val with_warning : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter   val with_error : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter   val with_failure : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter   val log :     ?kind:Log.kind -> ?verbose:int -> ?debug:int -> 'Log.pretty_printer   val with_log :     (Log.event -> 'b) -> ?kind:Log.kind -> ('a, 'b) Log.pretty_aborter   val register : Log.kind -> (Log.event -> unit) -> unit   val register_tag_handlers : (string -> string) * (string -> string) -> unit   val register_category : string -> Log.category   val get_category : string -> Log.Category_set.t   val get_all_categories : unit -> Log.Category_set.t   val add_debug_keys : Log.Category_set.t -> unit   val del_debug_keys : Log.Category_set.t -> unit   val get_debug_keys : unit -> Log.Category_set.t   val is_debug_key_enabled : Log.category -> bool   val get_debug_keyset : unit -> Log.category list   val add_group : ?memo:bool -> string -> Cmdline.Group.t   module Help : Parameter_sig.Bool   module Verbose : Parameter_sig.Int   module Debug : Parameter_sig.Int   module Debug_category : Parameter_sig.String_set   module Share : Parameter_sig.Specific_dir   module Session : Parameter_sig.Specific_dir   module Config : Parameter_sig.Specific_dir   val help : Cmdline.Group.t   val messages : Cmdline.Group.t   val reset : unit -> unit   module WP : Parameter_sig.Bool   module Behaviors : Parameter_sig.String_list   module Properties : Parameter_sig.String_list   module StatusAll : Parameter_sig.Bool   module StatusTrue : Parameter_sig.Bool   module StatusFalse : Parameter_sig.Bool   module StatusMaybe : Parameter_sig.Bool   type job =       WP_None     | WP_All     | WP_SkipFct of Cil_datatype.Kf.Set.t     | WP_Fct of Cil_datatype.Kf.Set.t   val job : unit -> Wp_parameters.job   val has_dkey : string -> bool   module Model : Parameter_sig.String_list   module ByValue : Parameter_sig.String_set   module ByRef : Parameter_sig.String_set   module InHeap : Parameter_sig.String_set   module InCtxt : Parameter_sig.String_set   module ExternArrays : Parameter_sig.Bool   module ExtEqual : Parameter_sig.Bool   module Literals : Parameter_sig.Bool   module Init : Parameter_sig.Bool   module InitWithForall : Parameter_sig.Bool   module BoundForallUnfolding : Parameter_sig.Int   module RTE : Parameter_sig.Bool   module Simpl : Parameter_sig.Bool   module Let : Parameter_sig.Bool   module Core : Parameter_sig.Bool   module Prune : Parameter_sig.Bool   module Clean : Parameter_sig.Bool   module Filter : Parameter_sig.Bool   module Bits : Parameter_sig.Bool   module QedChecks : Parameter_sig.String_set   module Split : Parameter_sig.Bool   module Invariants : Parameter_sig.Bool   module DynCall : Parameter_sig.Bool   module SimplifyIsCint : Parameter_sig.Bool   module SimplifyForall : Parameter_sig.Bool   module SimplifyType : Parameter_sig.Bool   module CalleePreCond : Parameter_sig.Bool   module Detect : Parameter_sig.Bool   module Generate : Parameter_sig.Bool   module Provers : Parameter_sig.String_list   module Drivers : Parameter_sig.String_list   module Script : Parameter_sig.String   module UpdateScript : Parameter_sig.Bool   module Timeout : Parameter_sig.Int   module CoqTimeout : Parameter_sig.Int   module CoqCompiler : Parameter_sig.String   module CoqIde : Parameter_sig.String   module CoqProject : Parameter_sig.String   module Depth : Parameter_sig.Int   module Steps : Parameter_sig.Int   module Procs : Parameter_sig.Int   module ProofTrace : Parameter_sig.Bool   module CoqLibs : Parameter_sig.String_list   module CoqTactic : Parameter_sig.String   module Hints : Parameter_sig.Int   module TryHints : Parameter_sig.Bool   module Why3 : Parameter_sig.String   module WhyLibs : Parameter_sig.String_list   module WhyFlags : Parameter_sig.String_list   module AltErgo : Parameter_sig.String   module AltGrErgo : Parameter_sig.String   module AltErgoLibs : Parameter_sig.String_list   module AltErgoFlags : Parameter_sig.String_list   module TruncPropIdFileName : Parameter_sig.Int   module Print : Parameter_sig.Bool   module Report : Parameter_sig.String_list   module ReportName : Parameter_sig.String   module Separation : Parameter_sig.Bool   module Check : Parameter_sig.Bool   val get_env : ?default:string -> string -> string   val is_out : unit -> bool   val get_output : unit -> string   val get_output_dir : string -> string   val get_includes : unit -> string list   val make_output_dir : string -> unit   val has_print_generated : unit -> bool   val print_generated : string -> unit end