Frama-C:
Plug-ins:
Libraries:

Frama-C API - Statistics

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

type ('k, 'ty) t

Type of statistics. Type parameter 'ty is either bound to int or float for integer and float statistics respectively and 'k show whether a statistic is tied:

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

Registered statistics

 

val memory_usage : (unit, int) t

Max heap size in kilobytes until the statistics are exported.

val alarm_count : (unit, int) t

Number of alarms emitted by the analysis.

val stmt_coverage : (unit, float) t

Ratio in 0, 1 of statements reached by the analysis to all statements in analyzed functions.

val fun_coverage : (unit, float) t

Ratio in 0, 1 of functions reached by the analysis to all functions in source files.

val analysis_duration : (unit, float) t

Analysis time of the main function, including children.

val iterations : (Frama_c_kernel.Cil_types.stmt, int) t

Number of times each statement has been interpreted.

Count of memexec cache hits.

val memexec_misses : (Frama_c_kernel.Cil_types.kernel_function, int) t

Count of memexec cache misses.

val max_widenings : (Frama_c_kernel.Cil_types.stmt, int) t

Maximum number of successive widening computed at each widening statement.

val max_unrolling : (Frama_c_kernel.Cil_types.stmt, int) t

Maximum number of loop unrolling computed at each loop statement.

val partitioning_index_hits : (unit, int) t

Count of state index hits.

val partitioning_index_misses : (unit, int) t

Count of state index misses.

Statistics registration

 

type _ typ =
  1. | Int : int typ
  2. | Float : float typ
val register_global_stat : string -> 'ty typ -> (unit, 'ty) t

Registers a statistic tied to the whole program.

val register_function_stat : string -> 'ty typ -> (Frama_c_kernel.Cil_types.kernel_function, 'ty) t

Registers a statistic tied to functions.

val register_statement_stat : string -> 'ty typ -> (Frama_c_kernel.Cil_types.stmt, 'ty) t

Registers a statistic tied to statements.

val add_compute_hook : (unit -> unit) -> unit

Add a hook function that will be called when the statistics are exported. Is can be used to update the statistics before they are actually used.

Statistics retrieval

 

val get : ('k, 'ty) t -> 'k -> 'ty

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

Statistics update

 

val set : ('k, 'ty) t -> 'k -> 'ty -> unit

Set the stat to the given value.

val incr : ('k, int) t -> 'k -> unit

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

val add : ('k, 'ty) t -> 'k -> 'ty -> unit

Add a custom amount to the stat or set it to this amount the stat is currently undefined.

val grow : ('k, 'ty) t -> 'k -> 'ty -> unit

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