package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

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

Module `Frama_c_kernel.Globals`

Operations on globals.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

module Vars : sig ... end

Globals variables. The AST should be computed before using this module (cf. Ast.compute).

module Functions : sig ... end

Functions. The AST should be computed before using this module (cf. Ast.compute).

module FileIndex : sig ... end

Globals associated to filename.

module Syntactic_search : sig ... end

Types

module Types : sig ... end

Types, or type-related information.

Entry point

exception No_such_entry_point of string

May be raised by entry_point below.

val entry_point : unit -> Cil_types.kernel_function * bool

returns
the current function entry point and a boolean indicating if it is a library entry point.

raises No_such_entry_point
if the current entrypoint name does not exist. This exception is automatically handled by the Frama-C kernel. Thus you don't have to catch it yourself, except if you do a specific work.

val set_entry_point : string -> bool -> unit

set_entry_point name lib sets Kernel.MainFunction to name and Kernel.LibEntry to lib. Moreover, clear the results of all the analysis which depend on Kernel.MainFunction or Kernel.LibEntry.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Comments

val get_comments_global : Cil_types.global -> string list

Gets a list of comments associated to the given global. This function is useful only when -keep-comments is on.

A comment is associated to a global if it occurs after the declaration/definition of the preceding one in the file, before the end of the current declaration/definition and does not occur in the definition of a function. Note that this function is experimental and may fail to associate comments properly. Use directly Cabshelper.Comments.get to retrieve comments in a given region. (see Globals.get_comments_stmt for retrieving comments associated to a statement).

since Nitrogen-20111001

val get_comments_stmt : Cil_types.stmt -> string list

Gets a list of comments associated to the given statement. This function is useful only when -keep-comments is on.

A comment is associated to a statement if it occurs after the preceding statement and before the current statement ends (except for the last statement in a block, to which statements occurring before the end of the block are associated). Note that this function is experimental and may fail to associate comments properly. Use directly Cabshelper.Comments.get to retrieve comments in a given region.

since Nitrogen-20111001

Getters

val get_annotation_name : Cil_types.global_annotation -> string option

Returns the name of the global annotation, when it exists (e.g. for axiomatics, predicates, etc), or None if no such name exists (e.g. for volatile blocks).

since 31.0-Gallium

val get_name : Cil_types.global -> string option

Returns the name of the global, when it exists (e.g. for variables, functions, types, etc), or None if no such name exists (e.g. for assembly statements).

since 31.0-Gallium

val get_statics : 
  (Cil_types.kernel_function -> Cil_types.varinfo list) Stdlib.ref

val find_first_stmt : (Cil_types.kernel_function -> Cil_types.stmt) Stdlib.ref

val find_enclosing_block : (Cil_types.stmt -> Cil_types.block) Stdlib.ref

val find_all_enclosing_blocks : 
  (Cil_types.stmt -> Cil_types.block list) Stdlib.ref

val find_englobing_kf : 
  (Cil_types.stmt -> Cil_types.kernel_function) Stdlib.ref

On This Page

Types
Entry point
Comments
Getters