sig
  type category
  type warn_category
  val verbose_atleast : int -> bool
  val debug_atleast : int -> bool
  val printf :
    ?level:int ->
    ?dkey:category ->
    ?current:bool ->
    ?source:Filepath.position ->
    ?append:(Format.formatter -> unit) ->
    ?header:(Format.formatter -> unit) ->
    ('a, Format.formatter, unit) format -> 'a
  val result : ?level:int -> ?dkey:category -> 'Log.pretty_printer
  val feedback :
    ?ontty:Log.ontty -> ?level:int -> ?dkey:category -> 'Log.pretty_printer
  val debug : ?level:int -> ?dkey:category -> 'Log.pretty_printer
  val warning : ?wkey:warn_category -> '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 option -> 'b) -> ('a, 'b) Log.pretty_aborter
  val with_warning : (Log.event option -> 'b) -> ('a, 'b) Log.pretty_aborter
  val with_error : (Log.event option -> 'b) -> ('a, 'b) Log.pretty_aborter
  val with_failure : (Log.event option -> 'b) -> ('a, 'b) Log.pretty_aborter
  val log :
    ?kind:Log.kind -> ?verbose:int -> ?debug:int -> 'Log.pretty_printer
  val logwith :
    (Log.event option -> 'b) ->
    ?wkey:warn_category ->
    ?emitwith:(Log.event -> unit) ->
    ?once:bool -> ('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 -> category
  val pp_category : Format.formatter -> category -> unit
  val dkey_name : category -> string
  val is_registered_category : string -> bool
  val get_category : string -> category option
  val get_all_categories : unit -> category list
  val add_debug_keys : category -> unit
  val del_debug_keys : category -> unit
  val get_debug_keys : unit -> category list
  val is_debug_key_enabled : category -> bool
  val get_debug_keyset : unit -> category list
  val register_warn_category : string -> warn_category
  val is_warn_category : string -> bool
  val pp_warn_category : Format.formatter -> warn_category -> unit
  val pp_all_warn_categories_status : unit -> unit
  val wkey_name : warn_category -> string
  val get_warn_category : string -> warn_category option
  val get_all_warn_categories : unit -> warn_category list
  val get_all_warn_categories_status :
    unit -> (warn_category * Log.warn_status) list
  val set_warn_status : warn_category -> Log.warn_status -> unit
  val get_warn_status : warn_category -> Log.warn_status
  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 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 add_plugin_output_aliases : string list -> unit
  val reset : unit -> unit
  type functions =
      Fct_none
    | Fct_all
    | Fct_skip of Cil_datatype.Kf.Set.t
    | Fct_list of Cil_datatype.Kf.Set.t
  val get_kf : unit -> Wp_parameters.functions
  val get_wp : unit -> Wp_parameters.functions
  val iter_fct :
    (Kernel_function.t -> unit) -> Wp_parameters.functions -> unit
  val iter_kf : (Kernel_function.t -> unit) -> unit
  val iter_wp : (Kernel_function.t -> 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
  val has_dkey : category -> 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 AliasInit : Parameter_sig.Bool
  module InCtxt : Parameter_sig.String_set
  module ExternArrays : Parameter_sig.Bool
  module Literals : Parameter_sig.Bool
  module Volatile : Parameter_sig.Bool
  module WeakIntModel : Parameter_sig.Bool
  module Region : Parameter_sig.Bool
  module Region_rw : Parameter_sig.Bool
  module Region_pack : Parameter_sig.Bool
  module Region_flat : Parameter_sig.Bool
  module Region_annot : Parameter_sig.Bool
  module Region_inline : Parameter_sig.Bool
  module Region_fixpoint : Parameter_sig.Bool
  module Region_cluster : 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 Parasite : Parameter_sig.Bool
  module Prenex : Parameter_sig.Bool
  module Bits : Parameter_sig.Bool
  module Ground : Parameter_sig.Bool
  module Reduce : Parameter_sig.Bool
  module ExtEqual : Parameter_sig.Bool
  module UnfoldAssigns : Parameter_sig.Bool
  module Split : Parameter_sig.Bool
  module SplitMax : Parameter_sig.Int
  module SplitDepth : Parameter_sig.Int
  module DynCall : Parameter_sig.Bool
  module SimplifyIsCint : Parameter_sig.Bool
  module SimplifyLandMask : Parameter_sig.Bool
  module SimplifyForall : Parameter_sig.Bool
  module SimplifyType : Parameter_sig.Bool
  module CalleePreCond : Parameter_sig.Bool
  module PrecondWeakening : Parameter_sig.Bool
  module Detect : Parameter_sig.Bool
  module Generate : Parameter_sig.Bool
  module Provers : Parameter_sig.String_list
  module RunAllProvers : Parameter_sig.Bool
  module Cache : Parameter_sig.String
  module CacheEnv : Parameter_sig.Bool
  module Drivers : Parameter_sig.String_list
  module Script : Parameter_sig.String
  module UpdateScript : Parameter_sig.Bool
  module Timeout : Parameter_sig.Int
  module SmokeTimeout : Parameter_sig.Int
  module TimeExtra : Parameter_sig.Int
  module TimeMargin : Parameter_sig.Int
  module CoqTimeout : Parameter_sig.Int
  module CoqCompiler : Parameter_sig.String
  module CoqIde : Parameter_sig.String
  module CoqProject : Parameter_sig.String
  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 Why3Flags : 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 Auto : Parameter_sig.String_list
  module AutoDepth : Parameter_sig.Int
  module AutoWidth : Parameter_sig.Int
  module BackTrack : Parameter_sig.Int
  module TruncPropIdFileName : Parameter_sig.Int
  module Print : Parameter_sig.Bool
  module Report : Parameter_sig.String_list
  module ReportJson : Parameter_sig.String
  module ReportName : Parameter_sig.String
  module MemoryContext : Parameter_sig.Bool
  module SmokeTests : Parameter_sig.Bool
  module SmokeDeadloop : Parameter_sig.Bool
  module SmokeDeadcode : Parameter_sig.Bool
  module SmokeDeadcall : Parameter_sig.Bool
  val has_out : unit -> bool
  val has_session : unit -> bool
  val get_session : force:bool -> unit -> Datatype.Filepath.t
  val get_session_dir : force:bool -> string -> Datatype.Filepath.t
  val get_output : unit -> Datatype.Filepath.t
  val get_output_dir : string -> Datatype.Filepath.t
  val make_output_dir : string -> unit
  val get_overflows : unit -> bool
  val has_print_generated : unit -> bool
  val print_generated : ?header:string -> string -> unit
  val cat_print_generated : category
end