Previous  Up  Next

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.

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.

val find_return : t -> Cil_types.stmt

Find the return statement of a kernel function.

val find_label : t -> string -> Cil_types.stmt Stdlib.ref

Find a given label in a kernel 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
val find_englobing_kf : Cil_types.stmt -> t
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.

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.

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

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.

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.

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.

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

Checkers

val is_definition : t -> bool
val is_in_libc : t -> bool
val is_entry_point : t -> bool
val is_main : t -> bool
val returns_void : t -> bool
val is_first_stmt : t -> Cil_types.stmt -> bool
val is_return_stmt : t -> Cil_types.stmt -> bool

Getters

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
val get_statics : t -> Cil_types.varinfo list

Returns the list of static variables declared inside the function.

exception No_Definition
val get_definition : t -> Cil_types.fundec
val has_definition : t -> bool

Membership of variables

val is_formal : Cil_types.varinfo -> t -> bool
val get_formal_position : Cil_types.varinfo -> t -> int

get_formal_position v kf is the position of v as parameter of kf.

val is_local : Cil_types.varinfo -> t -> bool
val is_formal_or_local : Cil_types.varinfo -> t -> bool
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 map = '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