Module Metrics_acsl

module Metrics_acsl: sig .. end

number of requires in function contracts

Visitor to compute various metrics about annotations

type acsl_stats = {

`mutable f_requires : int;`	`(*`	number of requires in function contractsnumber of requires in function contracts	`*)`
`mutable s_requires : int;`	`(*`	number of requires in statement contractsnumber of requires in statement contracts	`*)`
`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;`	`(*`	does not include loop assigns.does not include loop assigns.	`*)`
`mutable f_froms : int;`
`mutable s_froms : int;`	`(*`	does not include loop dependencies.does not include loop dependencies.	`*)`
`mutable invariants : int;`
`mutable loop_assigns : int;`
`mutable loop_froms : int;`
`mutable variants : int;`
`mutable asserts : int;`

}

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
type t = Metrics_acsl.acsl_stats 


val reprs : Metrics_acsl.acsl_stats list
val name : string
include Datatype.Serializable_undefined

val pretty : Format.formatter -> Metrics_acsl.acsl_stats -> unit
end)

module Global_acsl_stats: State_builder.Ref(Acsl_stats)(sig
val name : string
val dependencies : State.t list
val default : unit -> Metrics_acsl.acsl_stats
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