module Metrics_acsl:sig
..end
Visitor to compute various metrics about annotations
type
acsl_stats = {
|
mutable f_requires : |
(* | number of requires in function contracts number of requires in function contracts | *) |
|
mutable s_requires : |
(* | number of requires in statement contracts number of requires in statement contracts | *) |
|
mutable f_ensures : |
|||
|
mutable s_ensures : |
|||
|
mutable f_behaviors : |
|||
|
mutable s_behaviors : |
|||
|
mutable f_assumes : |
|||
|
mutable s_assumes : |
|||
|
mutable f_assigns : |
|||
|
mutable s_assigns : |
(* | does not include loop assigns. does not include loop assigns. | *) |
|
mutable f_froms : |
|||
|
mutable s_froms : |
(* | does not include loop dependencies. does not include loop dependencies. | *) |
|
mutable invariants : |
|||
|
mutable loop_assigns : |
|||
|
mutable loop_froms : |
|||
|
mutable variants : |
|||
|
mutable asserts : |
}
val empty_acsl_stat : unit -> acsl_stats
val incr_f_requires : acsl_stats -> unit
val incr_s_requires : acsl_stats -> unit
val incr_f_ensures : acsl_stats -> unit
val incr_s_ensures : acsl_stats -> unit
val incr_f_behaviors : acsl_stats -> unit
val incr_s_behaviors : acsl_stats -> unit
val incr_f_assumes : acsl_stats -> unit
val incr_s_assumes : acsl_stats -> unit
val incr_f_assigns : acsl_stats -> unit
val incr_s_assigns : acsl_stats -> unit
val incr_f_froms : acsl_stats -> unit
val incr_s_froms : acsl_stats -> unit
val incr_invariants : acsl_stats -> unit
val incr_loop_assigns : acsl_stats -> unit
val incr_loop_froms : acsl_stats -> unit
val incr_variants : acsl_stats -> unit
val incr_asserts : acsl_stats -> unit
val pretty_acsl_stats : Stdlib.Format.formatter -> acsl_stats -> unit
val pretty_acsl_stats_html : Stdlib.Format.formatter -> acsl_stats -> unit
val get_global_stats : unit -> acsl_stats
val get_kf_stats : Kernel_function.t -> acsl_stats
val dump_acsl_stats : Stdlib.Format.formatter -> unit
val dump_acsl_stats_html : Stdlib.Format.formatter -> unit
val dump : unit -> unit