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 there is no return statement for the given function.
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 clear_sid_info : unit -> unit

removes any information related to statements in kernel functions. ( the table used by the function below).

Must be called when the Ast has silently changed (e.g. with an in-place visitor) before calling one of the functions below
Use with caution, as it is very expensive to re-populate the table.

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 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.

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 returns_void : t -> bool

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

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.

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

val self : State.t