Module Kernel_function

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.
Consult the Plugin Development Guide for additional details.


Kernel functions are comparable and hashable


include Datatype.S_with_collections
val id : t -> int
val auxiliary_kf_stmt_state : State.t

Searching


exception No_Statement
val find_first_stmt : t -> Cil_types.stmt
Find the first statement in a kernel function.
Raises 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.
Raises No_Statement is the kernel function is only a prototype.
Change in Nitrogen-20111001: may raise No_Statement
val find_label : t -> string -> Cil_types.stmt Pervasives.ref
Find a given label in a kernel function.
Raises 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.
Since Chlorine-20180501
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.
Since Chlorine-20180501
val find_from_sid : int -> Cil_types.stmt * t
Raises Not_found if there is no statement with such an identifier.
Returns the stmt and its kernel function from its identifier. Complexity: the first call to this function is linear in the size of the cil file.
val find_englobing_kf : Cil_types.stmt -> t
Raises Not_found if the given statement is not correctly registered
Returns the function to which the statement belongs. Same complexity as find_from_sid
val find_enclosing_block : Cil_types.stmt -> Cil_types.block
Returns the innermost block to which the given statement belongs.
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.
Since Carbon-20101201
Raises 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.
Since Magnesium-20151001
Raises 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.
Since 19.0-Potassium
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.
Since Oxygen-20120901
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
Since Oxygen-20120901
Raises 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.
Since Carbon-20110201
Returns a list of 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.
Since 20.0-Calcium
Raises 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.
Since 19.0-Potassium
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.
Since 19.0-Potassium
Raises 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).
Since 19.0-Potassium
Raises AbortFatal if pre-conditions are not met.

Checkers


val is_definition : t -> bool
val is_entry_point : t -> bool
Since Sodium-20150201
Returns true iff the given function is the main of the program (as stated by option -main).
val is_main : t -> bool
Since 21.0-Scandium
Returns true iff the given function is the function called 'main' in the program.
val returns_void : t -> bool
val is_first_stmt : t -> Cil_types.stmt -> bool
Since 21.0-Scandium
Returns true iff the statement is the first statement of the given function.
val is_return_stmt : t -> Cil_types.stmt -> bool
Since 21.0-Scandium
Returns true iff the statement is the return statement of the given function.

Getters


val dummy : unit -> t
Consult the Plugin Development Guide for additional details.
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
val get_statics : t -> Cil_types.varinfo list
Returns the list of static variables declared inside the function.
Since 18.0-Argon
exception No_Definition
val get_definition : t -> Cil_types.fundec
Raises No_Definition if the given function is not a definition.
Consult the Plugin Development Guide for additional details.
val has_definition : t -> bool
Since 21.0-Scandium
Returns true iff the given kernel function has a defintion.

Membership of variables


val is_formal : Cil_types.varinfo -> t -> bool
Returns 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.
Raises Not_found if v is not a formal of kf.
val is_local : Cil_types.varinfo -> t -> bool
Returns 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
Returns 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.

Collections


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.

Setters

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