module Metrics_base:sig
..end
Defining base metrics and operations on those
val html_stag_functions : Transitioning.Format.formatter_stag_functions
val mk_hdr : int -> Format.formatter -> string -> unit
level
ppf
hdr_strg
produces a title from hdr_strg
with an
underline of the same length.
The character of the underline is set according to level
:module OptionKf:Datatype.S_with_collections
with type t = Kernel_function.t option
module BasicMetrics:sig
..end
module VInfoMap:Map.S
with type key = Cil_types.varinfo
module VInfoSet:Set.S
with type elt = Cil_types.varinfo
val pretty_set : Format.formatter -> int VInfoMap.t -> unit
Other pretty-printing and formatting utilities
val pretty_extern_vars : Format.formatter -> VInfoSet.t -> unit
val number_entry_points : int VInfoMap.t -> int
val pretty_entry_points : Format.formatter -> int VInfoMap.t -> unit
val file_of_vinfodef : Cil_types.varinfo -> Datatype.Filepath.t
val file_of_fundef : Cil_types.fundec -> Datatype.Filepath.t
val extract_fundef_name : Cabs.single_name -> string
val kf_of_cabs_name : Cabs.single_name -> Kernel_function.t
val get_filename : Cabs.definition -> Datatype.Filepath.t
type
output_type =
| |
Html |
| |
Text |
val get_file_type : string -> output_type
extension
sets the output type according to extension
.
Raises an error if extension
is not among supported extensions or is empty.val consider_function : libc:bool -> Cil_types.varinfo -> bool
vinfo
returns false if the varinfo is not a function we
are interested in.
For example, builtins should not be part of the analysis and return false.
If libc
is false, do not consider functions from the Frama-C libc.
Skip them using this auxiliary function.val consider_variable : libc:bool -> Cil_types.varinfo -> bool
consider_variable vinfo
returns false if the varinfo is not an object
variable we are interested in. Currently excluded variables are those
declared with attribute __FRAMA_C_MODEL__
.
If libc
is false, do not consider variables from the Frama-C libc.val float_to_string : float -> string