module Kernel_function:sig
..end
Operations to get info from a kernel function. This module does
not give access to information about the set of all the registered kernel
functions (like iterators over kernel functions). This kind of operations is
stored in module Globals.Functions
.
include Datatype.S_with_collections
val id : t -> int
val auxiliary_kf_stmt_state : State.t
exception No_Statement
val find_first_stmt : t -> Cil_types.stmt
Find the first statement in a kernel function.
No_Statement
if there is no first statement for the given
function.val find_return : t -> Cil_types.stmt
Find the return statement of a kernel function.
No_Statement
is the kernel function is only a prototype.val find_label : t -> string -> Cil_types.stmt Pervasives.ref
Find a given label in a kernel function.
Not_found
if the label does not exist in the given function.val find_all_labels : t -> Datatype.String.Set.t
returns all labels present in a given function.
val clear_sid_info : unit -> unit
removes any information related to statements in kernel functions. ( the table used by the function below).
val find_defining_kf : Cil_types.varinfo -> t option
Finds the kernel function defining the given varinfo as a local or a formal. Returns None if no such function exists.
val find_from_sid : int -> Cil_types.stmt * t
Not_found
if there is no statement with such an identifier.val find_englobing_kf : Cil_types.stmt -> t
Not_found
if the given statement is not correctly registeredfind_from_sid
val find_enclosing_block : Cil_types.stmt -> Cil_types.block
val find_all_enclosing_blocks : Cil_types.stmt -> Cil_types.block list
same as above, but returns all enclosing blocks, starting with the innermost one.
val blocks_closed_by_edge : Cil_types.stmt -> Cil_types.stmt -> Cil_types.block list
blocks_closed_by_edge s1 s2
returns the (possibly empty)
list of blocks that are closed when going from s1
to s2
.
Invalid_argument
if s2
is not a successor of s1
in the cfg.val blocks_opened_by_edge : Cil_types.stmt -> Cil_types.stmt -> Cil_types.block list
blocks_opened_by_edge s1 s2
returns the (possibly empty)
list of blocks that are opened when going from s1
to s2
.
Invalid_argument
if s2
is not a successor of s1
in the cfg.val stmt_in_loop : t -> Cil_types.stmt -> bool
stmt_in_loop kf stmt
is true
iff stmt
strictly
occurs in a loop of kf
.
val find_enclosing_loop : t -> Cil_types.stmt -> Cil_types.stmt
find_enclosing_loop kf stmt
returns the statement corresponding
to the innermost loop containing stmt
in kf
. If stmt
itself is
a loop, returns stmt
Not_found
if stmt
is not part of a loop of kf
val find_syntactic_callsites : t -> (t * Cil_types.stmt) list
callsites f
collect the statements where f
is called. Same
complexity as find_from_sid
.
f',s
where function f'
calls f
at statement
stmt
.val is_definition : t -> bool
val is_entry_point : t -> bool
val returns_void : t -> bool
val dummy : unit -> t
val get_vi : t -> Cil_types.varinfo
val get_id : t -> int
val get_name : t -> string
val get_type : t -> Cil_types.typ
val get_return_type : t -> Cil_types.typ
val get_location : t -> Cil_types.location
val get_global : t -> Cil_types.global
For functions with a declaration and a definition, returns the definition.
val get_formals : t -> Cil_types.varinfo list
val get_locals : t -> Cil_types.varinfo list
exception No_Definition
val get_definition : t -> Cil_types.fundec
No_Definition
if the given function is not a definition.val is_formal : Cil_types.varinfo -> t -> bool
true
if the given varinfo is a formal parameter of the given
function. If possible, use this function instead of
Ast_info.Function.is_formal
.val get_formal_position : Cil_types.varinfo -> t -> int
get_formal_position v kf
is the position of v
as parameter of kf
.
Not_found
if v
is not a formal of kf
.val is_local : Cil_types.varinfo -> t -> bool
true
if the given varinfo is a local variable of the given
function. If possible, use this function instead of
Ast_info.Function.is_local
.val is_formal_or_local : Cil_types.varinfo -> t -> bool
true
if the given varinfo is a formal parameter or a local
variable of the given function.
If possible, use this function instead of
Ast_info.Function.is_formal_or_local
.val get_called : Cil_types.exp -> t option
Returns the static call to function expr
, if any.
None
means a dynamic call through function pointer.
module Make_Table:functor (
Data
:
Datatype.S
) ->
functor (
Info
:
State_builder.Info_with_size
) ->
State_builder.Hashtbl
with type key = t and type data = Data.t
Hashtable indexed by kernel functions and dealing with project.
module Hptset:Hptset.S
with type elt = kernel_function and type 'a shape = 'a Hptmap.Shape(Cil_datatype.Kf).t
Set of kernel functions.
Use carefully the following functions.
val register_stmt : t -> Cil_types.stmt -> Cil_types.block list -> unit
Register a new statement in a kernel function, with the list of blocks that contain the statement (innermost first).
val self : State.t