module Kernel_function:sig
..end
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
No_Statement
if there is no first statement for the given
function.val find_return : t -> Cil_types.stmt
No_Statement
is the kernel function is only a prototype.val find_label : t -> string -> Cil_types.stmt Pervasives.ref
Not_found
if the label does not exist in the given function.val find_all_labels : t -> Datatype.String.Set.t
val clear_sid_info : unit -> unit
val find_defining_kf : Cil_types.varinfo -> t option
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
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 common_block : Cil_types.stmt -> Cil_types.stmt -> Cil_types.block
common_block s1 s2
returns the innermost block that contains
both s1
and s2
, provided the statements belong to the same function.
raises a fatal error if this is not the case.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 local_definition : t -> Cil_types.varinfo -> Cil_types.stmt
local_definition f v
returns the statement initializing the (defined)
local variable v
of f
.AbortFatal
if v
is not defined or is not a local of f
val var_is_in_scope : Cil_types.stmt -> Cil_types.varinfo -> bool
var_is_in_scope kf stmt vi
returns true
iff the local variable vi
is syntactically visible from statement stmt
in function kf
. Note
that on the contrary to Globals.Syntactic_search.find_in_scope
, the
variable is searched according to its vid
, not its vorig_name
.val find_enclosing_stmt_in_block : Cil_types.block -> Cil_types.stmt -> Cil_types.stmt
find_enclosing_stmt_in_block b s
returns the statements s'
inside b.bstmts
that contains s
. It might be s
itself, but also
an inner block (recursively) containing s
.AbortFatal
if b
is not equal to find_enclosing_block s
val is_between : Cil_types.block -> Cil_types.stmt -> Cil_types.stmt -> Cil_types.stmt -> bool
is_between b s1 s2 s3
returns true
if the statement s2
appears
strictly between s1
and s3
inside the b.bstmts
list.
All three statements
must actually occur in b.bstmts
, either directly or indirectly
(see Kernel_function.find_enclosing_stmt_in_block
).AbortFatal
if pre-conditions are not met.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
val get_formals : t -> Cil_types.varinfo list
val get_locals : t -> Cil_types.varinfo list
val get_statics : 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
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
module Hptset:Hptset.S
with type elt = kernel_function and type 'a shape = 'a Hptmap.Shape(Cil_datatype.Kf).t
Use carefully the following functions.
val register_stmt : t -> Cil_types.stmt -> Cil_types.block list -> unit
val self : State.t