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 : |
(* | syntactically reachable functions | *) |
|
semantic : |
(* | semantically reachable functions | *) |
|
initializers : |
(* | initializers | *) |
}
val percent_coverage : libc:bool -> 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.