Module Metrics_cilast

module Metrics_cilast: sig .. end

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


class type sloc_visitor = object .. end

Visitor to compute various syntactic metrics.

class slocVisitor : libc:bool -> sloc_visitor
val get_global_metrics : libc:bool -> Metrics_base.BasicMetrics.t

Returns the computed metrics for the entire AST.

type cilast_metrics = {
   fundecl_calls : int Metrics_base.VInfoMap.t;
   funspec_calls : int Metrics_base.VInfoMap.t;
   fundef_calls : int Metrics_base.VInfoMap.t;
   extern_global_vars : Metrics_base.VInfoSet.t;
   basic_global_metrics : Metrics_base.BasicMetrics.t;
}
val get_cilast_metrics : libc:bool -> cilast_metrics
val get_metrics_map : libc:bool ->
Metrics_base.BasicMetrics.t Metrics_base.OptionKf.Map.t
Datatype.Filepath.Map.t

Computes and returns individual metrics per function.

val compute_on_cilast : libc:bool -> unit

Compute metrics on whole CIL AST

val compute_locals_size : Kernel_function.t -> unit

Compute and print the size (in bytes) of local variables on the CIL AST. This is a rough approximation, neither guaranteed to be smaller or larger than the actual value. Only automatic, non-ghost and non-temporary variables present in the source are included. This is useful to estimate the stack size of a function.

val reachable_from_main : unit -> Cil_types.varinfo list option

Computes the set of global variables which are syntactically reachable from the entry point of the program. Returns None if there is no entry point.

val used_files : unit -> Datatype.Filepath.Set.t

Computes the set of files defining all global variables syntactically reachable from the entry point of the program (as given by reachable_from_main). This function requires a defined entry point.

val pretty_used_files : Datatype.Filepath.Set.t -> unit

Pretty-prints the result of used_files in a verbose way.