Frama-C:
Plug-ins:
Libraries:

Frama-C API - Statistics

This module keeps track of statistics collected by Eva during an analysis.

type 'a t

Type of statistics. Type parameter 'a show whether a statistic is tied:

  • to kernel_function,
  • to Cil stmt,
  • to the whole program, with unit.

Registered statistics

 

val max_widenings : Frama_c_kernel.Cil_types.stmt t
val max_unrolling : Frama_c_kernel.Cil_types.stmt t
val partitioning_index_hits : unit t
val partitioning_index_misses : unit t

Statistics registration

 

val register_global_stat : string -> unit t

Registers a statistic tied to the whole program.

val register_function_stat : string -> Frama_c_kernel.Cil_types.kernel_function t

Registers a statistic tied to functions.

val register_statement_stat : string -> Frama_c_kernel.Cil_types.stmt t

Registers a statistic tied to statements.

Statistics retrieval

 

val get : 'a t -> 'a -> int

Get the current stat value for a given element (statement, function or unit according to the statistic type). *

Statistics update

 

val set : 'a t -> 'a -> int -> unit

Set the stat to the given value.

val incr : 'a t -> 'a -> unit

Adds 1 to the stat or set it to 1 if undefined.

val grow : 'a t -> 'a -> int -> unit

Set the stat to the maximum between the current value and the given value.