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.