Frama-C:
Plug-ins:
Libraries:

Frama-C API - Summary

Summary

type alarm_category =
  1. | Division_by_zero
  2. | Memory_access
  3. | Index_out_of_bound
  4. | Unaligned_pointer
  5. | Invalid_shift
  6. | Overflow
  7. | Uninitialized
  8. | Dangling
  9. | Nan_or_infinite
  10. | Float_to_int
  11. | Other
type coverage = {
  1. mutable reachable : int;
  2. mutable dead : int;
}
type statuses = {
  1. mutable valid : int;
  2. mutable unknown : int;
  3. mutable invalid : int;
}
type events = {
  1. mutable errors : int;
  2. mutable warnings : int;
}
type alarms = (alarm_category * int) list
type fun_stats = {
  1. fun_coverage : coverage;
  2. fun_alarm_count : alarms;
  3. fun_alarm_statuses : statuses;
}
type program_stats = {
  1. prog_fun_coverage : coverage;
  2. prog_stmt_coverage : coverage;
  3. prog_alarms : alarms;
  4. eva_events : events;
  5. kernel_events : events;
  6. alarms_statuses : statuses;
  7. assertions_statuses : statuses;
  8. preconds_statuses : statuses;
}
module FunctionStats : sig ... end
val compute_stats : unit -> program_stats

Compute analysis statistics.

val print : unit -> unit

Prints a summary of the analysis.