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 -> 'a Log.pretty_printer
val feedback :
?ontty:Log.ontty -> ?level:int -> ?dkey:category -> 'a Log.pretty_printer
val debug : ?level:int -> ?dkey:category -> 'a Log.pretty_printer
val warning : ?wkey:warn_category -> 'a Log.pretty_printer
val error : 'a Log.pretty_printer
val abort : ('a, 'b) Log.pretty_aborter
val failure : 'a 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 -> ('a -> 'b) -> 'a -> '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 -> 'a 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 :
?visible:bool -> ?deprecated:bool -> 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_fct : unit -> Wp.Wp_parameters.functions
val iter_fct :
(Kernel_function.t -> unit) -> Wp.Wp_parameters.functions -> unit
val iter_kf : (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 FilterInit : 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 Interactive : Parameter_sig.String
module RunAllProvers : Parameter_sig.Bool
module Cache : Parameter_sig.String
module CacheEnv : Parameter_sig.Bool
module CacheDir : Parameter_sig.String
module CachePrint : 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 InteractiveTimeout : 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 CheckMemoryContext : 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
val protect : exn -> bool
end