package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Eva.Statistics

Various statistics collected during an analysis.

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.

val reset_all : unit -> unit

Reset all statistics to zero.

Export

 

val export_as_csv : ?filename:Frama_c_kernel.Filepath.t -> unit -> unit

Export the computed statistics as CSV.