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 : Format.formatter -> acsl_stats -> unit
val pretty_acsl_stats_html : Format.formatter -> acsl_stats -> unit
module Acsl_stats:Datatype.Make
(
sig
typet =
Metrics_acsl.acsl_stats
val reprs :Metrics_acsl.acsl_stats list
val name :string
include Datatype.Serializable_undefinedval pretty :Format.formatter -> Metrics_acsl.acsl_stats -> unit
end
)
module Global_acsl_stats:State_builder.Ref
(
Acsl_stats
)
(
sig
end
)
module Functions_acsl_stats:State_builder.Hashtbl
(
Kernel_function.Hashtbl
)
(
Acsl_stats
)
(
sig
val name :string
val dependencies :State.t list
val size :int
end
)
val get_kf_stats : Functions_acsl_stats.key ->
Functions_acsl_stats.data
module Computed:State_builder.False_ref
(
sig
val name :string
val dependencies :State.t list
end
)
val treat_behavior : Global_acsl_stats.data ->
Cil_types.kinstr -> ('a, 'b) Cil_types.behavior -> unit
val add_function_contract_stats : Functions_acsl_stats.key -> unit
val add_code_annot_stats : Cil_types.stmt -> 'a -> Cil_types.code_annotation -> unit
val compute : unit -> unit
val get_global_stats : unit -> Global_acsl_stats.data
val dump_html_global : Format.formatter -> unit
val dump_html_by_function : Format.formatter -> unit
val dump_acsl_stats : Format.formatter -> unit
val dump_acsl_stats_html : Format.formatter -> unit
val dump : unit -> unit