debug.mli 3.39 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18 19 20
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

type flag
21
(* Flag used for debugging only part of Why3 *)
22 23

val register_flag : string -> flag
24 25 26
(** Register a new flag. If someone try to register two times the same
    flag the same one is used *)

27 28 29 30 31 32
val register_stop_flag : string -> flag
(** Register a new stop flag. If someone try to register two times the same
    flag the same one is used.
    A stop flag should be used when a flag change the behavior of the program.
    It is not setted by debug-all *)

33 34
val lookup_flag : string -> flag
val list_flags : unit -> (string * flag * bool) list
35
(** List the known flags *)
36

37 38 39
val is_stop_flag : string -> bool
(** test if the flag is a stop flag *)

40
(** Modify the state of a flag *)
41 42 43 44 45
val set_flag : flag -> unit
val unset_flag : flag -> unit
val toggle_flag : flag -> unit

val test_flag : flag -> bool
46 47 48 49 50 51
(** Return the state of the flag *)
val nottest_flag : flag -> bool

val set_debug_formatter : Format.formatter -> unit
(** Set the formatter used when printing debug material *)

52 53 54 55
val get_debug_formatter : unit -> Format.formatter
(** Get the formatter used when printing debug material *)


56 57
val dprintf : flag -> ('a, Format.formatter, unit) format -> 'a
(** Print only if the flag is set *)
58

59
val stack_trace : flag
60
(** stack_trace flag *)
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88

(** Command line arguments *)
module Opt : sig
  type spec = (Arg.key * Arg.spec * Arg.doc)

  val desc_debug_list : spec
  (** Option for printing the list of debug flags *)

  val option_list : unit -> bool
  (** Print the list of debug flag if requested (in this case return [true]).
      You should run this function after the plugins have been started.
  *)

  val desc_debug_all : spec
  (** Option for setting all the debug flags except the stopping one *)

  val desc_debug : spec
  (** Option for specifying a debug flag to set *)

  val desc_shortcut : string -> Arg.key -> Arg.doc -> spec
  (** Option for setting a specific flag *)

  val set_flags_selected : unit -> unit
  (** Set the flags selected by debug_all, debug or a shortcut.
      You should run this function after the plugins have been started.
  *)

end