sig
type alarm_category =
Division_by_zero
| Memory_access
| Index_out_of_bound
| Invalid_shift
| Overflow
| Uninitialized
| Dangling
| Nan_or_infinite
| Float_to_int
| Other
type coverage = { mutable reachable : int; mutable dead : int; }
type statuses = {
mutable valid : int;
mutable unknown : int;
mutable invalid : int;
}
type events = { mutable errors : int; mutable warnings : int; }
type alarms = (Summary.alarm_category * int) list
type fun_stats = {
fun_coverage : Summary.coverage;
fun_alarm_count : Summary.alarms;
fun_alarm_statuses : Summary.statuses;
}
type program_stats = {
prog_fun_coverage : Summary.coverage;
prog_stmt_coverage : Summary.coverage;
prog_alarms : Summary.alarms;
eva_events : Summary.events;
kernel_events : Summary.events;
alarms_statuses : Summary.statuses;
assertions_statuses : Summary.statuses;
preconds_statuses : Summary.statuses;
}
module FunctionStats :
sig
val get : Cil_types.fundec -> Summary.fun_stats option
val iter : (Cil_types.fundec -> Summary.fun_stats -> unit) -> unit
val recompute : Cil_types.fundec -> unit
val register_hook :
(Cil_types.fundec * Summary.fun_stats -> unit) -> unit
end
val compute_stats : unit -> Summary.program_stats
val print_summary : unit -> unit
end