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.