Module Globals

module Globals: sig .. end
Operations on globals.
Consult the Plugin Development Guide for additional details.

module Vars: sig .. end
Globals variables.
module Functions: sig .. end
Functions.
module FileIndex: sig .. end
Globals associated to filename.

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
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.
Returns the current function entry point and a boolean indicating if it is a library entry point.
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.
Consult the Plugin Development Guide for additional details.

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 global. This function is useful only when -keep-comments is on.

A comment is associated to a global if it occurs after the preceding statement and before the current statement ends (except for the last statement in a block, to which statements occuring 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

val find_first_stmt : (Cil_types.kernel_function -> Cil_types.stmt) Pervasives.ref
val find_enclosing_block : (Cil_types.stmt -> Cil_types.block) Pervasives.ref