module Globals:sig
..end
Operations on globals.
module Vars:sig
..end
Globals variables.
module Functions:sig
..end
Functions.
module FileIndex:sig
..end
Globals associated to filename.
module Syntactic_search:sig
..end
module Types:sig
..end
Types, or type-related information.
exception No_such_entry_point of string
May be raised by entry_point
below.
val entry_point : unit -> Cil_types.kernel_function * bool
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
.
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).
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.
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