sig
  type acsl_stats = {
    mutable f_requires : int;
    mutable s_requires : int;
    mutable f_ensures : int;
    mutable s_ensures : int;
    mutable f_behaviors : int;
    mutable s_behaviors : int;
    mutable f_assumes : int;
    mutable s_assumes : int;
    mutable f_assigns : int;
    mutable s_assigns : int;
    mutable f_froms : int;
    mutable s_froms : int;
    mutable invariants : int;
    mutable loop_assigns : int;
    mutable loop_froms : int;
    mutable variants : int;
    mutable asserts : int;
  }
  val empty_acsl_stat : unit -> Metrics_acsl.acsl_stats
  val incr_f_requires : Metrics_acsl.acsl_stats -> unit
  val incr_s_requires : Metrics_acsl.acsl_stats -> unit
  val incr_f_ensures : Metrics_acsl.acsl_stats -> unit
  val incr_s_ensures : Metrics_acsl.acsl_stats -> unit
  val incr_f_behaviors : Metrics_acsl.acsl_stats -> unit
  val incr_s_behaviors : Metrics_acsl.acsl_stats -> unit
  val incr_f_assumes : Metrics_acsl.acsl_stats -> unit
  val incr_s_assumes : Metrics_acsl.acsl_stats -> unit
  val incr_f_assigns : Metrics_acsl.acsl_stats -> unit
  val incr_s_assigns : Metrics_acsl.acsl_stats -> unit
  val incr_f_froms : Metrics_acsl.acsl_stats -> unit
  val incr_s_froms : Metrics_acsl.acsl_stats -> unit
  val incr_invariants : Metrics_acsl.acsl_stats -> unit
  val incr_loop_assigns : Metrics_acsl.acsl_stats -> unit
  val incr_loop_froms : Metrics_acsl.acsl_stats -> unit
  val incr_variants : Metrics_acsl.acsl_stats -> unit
  val incr_asserts : Metrics_acsl.acsl_stats -> unit
  val pretty_acsl_stats : Format.formatter -> Metrics_acsl.acsl_stats -> unit
  val pretty_acsl_stats_html :
    Format.formatter -> Metrics_acsl.acsl_stats -> unit
  val get_global_stats : unit -> Metrics_acsl.acsl_stats
  val get_kf_stats : Kernel_function.t -> Metrics_acsl.acsl_stats
  val dump_acsl_stats : Format.formatter -> unit
  val dump_acsl_stats_html : Format.formatter -> unit
  val dump : unit -> unit
end