package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Kernel functions are comparable and hashable
Searching
Checkers
Getters
Membership of variables
Collections
Setters

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.0-beta-Nickel.tar.gz

sha256=0c80dae8074fcb3f6a33d7a41faf9939a2a336478a8d2c79e20e2d7bab953735

doc/frama-c.kernel/Frama_c_kernel/Kernel_function/index.html

Module `Frama_c_kernel.Kernel_function`

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

Kernel functions are comparable and hashable

include Datatype.S_with_collections
  with type t = Cil_types.kernel_function
   and module Set = Cil_datatype.Kf.Set
   and module Map = Cil_datatype.Kf.Map
   and module Hashtbl = Cil_datatype.Kf.Hashtbl

include Datatype.S with type t = Cil_types.kernel_function

include Datatype.S_no_copy with type t = Cil_types.kernel_function

include Datatype.Ty with type t = Cil_types.kernel_function

type t = Cil_types.kernel_function

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val ty : t Type.t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

module Set = Cil_datatype.Kf.Set

module Map = Cil_datatype.Kf.Map

module Hashtbl = Cil_datatype.Kf.Hashtbl

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.

val find_label : t -> string -> Cil_types.stmt 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. (i.e. 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_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

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.

raises Not_found
if there is no statement with such an identifier.

val find_englobing_kf : Cil_types.stmt -> t

returns
the function to which the statement belongs. Same complexity as find_from_sid

raises Not_found
if the given statement is not correctly registered

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.

raises Invalid_argument
if s2 is not a successor of s1 in the cfg.

since Carbon-20101201

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.

raises Invalid_argument
if s2 is not a successor of s1 in the cfg.

since Magnesium-20151001

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

raises Not_found
if stmt is not part of a loop of kf

since Oxygen-20120901

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.

returns
a list of f',s where function f' calls f at statement stmt.

since Carbon-20110201

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.

raises AbortFatal
if v is not defined or is not a local of f

since 20.0-Calcium

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.

raises AbortFatal
if b is not equal to find_enclosing_block s

since 19.0-Potassium

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

raises AbortFatal
if pre-conditions are not met.

since 19.0-Potassium

Checkers

val is_definition : t -> bool

val is_in_libc : t -> bool

returns
true iff the given function attributes contain libc indicators.

since 24.0-Chromium

val is_not_called : t -> bool

returns
true if the given function is not called in the program. Warning, return false does not ensure that the function is called.

since 28.0-Nickel

val is_entry_point : t -> bool

returns
true iff the given function is the main of the program (as stated by option -main).

since Sodium-20150201

val is_main : t -> bool

returns
true iff the given function is the function called 'main' in the program.

since 21.0-Scandium

val returns_void : t -> bool

val is_first_stmt : t -> Cil_types.stmt -> bool

returns
true iff the statement is the first statement of the given function.

since 21.0-Scandium

val is_return_stmt : t -> Cil_types.stmt -> bool

returns
true iff the statement is the return statement of the given function.

since 21.0-Scandium

Getters

val dummy : unit -> t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val get_vi : t -> Cil_types.varinfo

val get_id : t -> int

returns
the identifier of the function (which is the identifier of the associated varinfo).

val get_name : t -> string

val get_type : t -> Cil_types.typ

Be careful! The return type, as normalized by Cabs2Cil does not have any qualifier at first level (e.g no ghost).

returns
the type of the given kernel function

val get_return_type : t -> Cil_types.typ

Be careful! The return type, as normalized by Cabs2Cil does not have any qualifier at first level (e.g no ghost).

returns
the return type of the function

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val has_definition : t -> bool

returns
true iff the given kernel function has a defintion.

since 21.0-Scandium

val is_ghost : t -> bool

returns
true iff the given kernel function is ghost

since 26.0-Iron

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
  (Data : Datatype.S)
  (_ : 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 = Cil_types.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

val self : State.t