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 -> 'a Log.pretty_printer
val feedback :
?ontty:Log.ontty ->
?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer
val debug : ?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer
val warning : '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 -> '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 -> 'a 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 : Log.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 InCtxt : Parameter_sig.String_set
module ExternArrays : Parameter_sig.Bool
module ExtEqual : Parameter_sig.Bool
module Overflows : Parameter_sig.Bool
module Literals : Parameter_sig.Bool
module Volatile : Parameter_sig.Bool
module Init : Parameter_sig.Bool
module InitAlias : 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 QedChecks : Parameter_sig.String_set
module Split : Parameter_sig.Bool
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 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 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 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_session : unit -> string
val get_session_dir : string -> string
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 : ?header:string -> string -> unit
end