Module Metrics_coverage

module Metrics_coverage: sig .. end

In the definitions below, setting argument libc to true will include functions/variables from the C stdlib in the metrics.

val compute_syntactic : libc:bool -> Kernel_function.t -> Cil_datatype.Varinfo.Set.t

List of functions that can be syntactically reached from the function

val compute_semantic : libc:bool -> Cil_datatype.Varinfo.Set.t

Functions analyzed by the value analysis

type coverage_metrics = {

`syntactic : Cil_datatype.Varinfo.Set.t;`	`(*`	syntactically reachable functions	`*)`
`semantic : Cil_datatype.Varinfo.Set.t;`	`(*`	semantically reachable functions	`*)`
`initializers : (Cil_types.varinfo * Cil_types.init) list;`	`(*`	initializers	`*)`

}

val percent_coverage : coverage_metrics -> float

val compute : libc:bool -> coverage_metrics

Computes both syntactic and semantic coverage information.

val compute_coverage_by_fun : unit -> unit

Computes the semantic coverage by function.

val get_coverage : Kernel_function.t -> int * int * float

Returns the coverage for a given function. Raises Not_found if it has not been computed for the function.

val is_computed_by_fun : unit -> bool

val clear_coverage_by_fun : unit -> unit

class syntactic_printer : libc:bool -> Cil_datatype.Varinfo.Set.t -> object .. end

Pretty-printer for syntactic coverage metrics.

class semantic_printer : libc:bool -> coverage_metrics -> object .. end

Pretty-printer for semantic coverage metrics.