package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Internals

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-Nickel.tar.gz

sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

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

Module `Frama_c_kernel.Ast`

Access to the CIL AST which must be used from Frama-C.

exception Bad_Initialization of string

May be raised by function get below.

exception NoUntypedAst

Might be raised by UntypedFiles.get below

since Nitrogen-20111001

module UntypedFiles : sig ... end

val get : unit -> Cil_types.file

Get the cil file representation. One of the initialization function of module File has to be called before using this function.

raises Bad_Initialization
if neither File.init_from_c_files nor File.init_project_from_cil_file nor File.init_from_cmdline was called before.

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

val compute : unit -> unit

Enforce the computation of the AST.

raises Bad_Initialization
if neither File.init_from_c_files nor File.init_project_from_cil_file nor File.init_from_cmdline was called before.

val is_computed : unit -> bool

returns
true if the AST has been computed.

val mark_as_changed : unit -> unit

call this function whenever you've made some changes in place inside the AST

since Oxygen-20120901

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

val mark_as_grown : unit -> unit

call this function whenever you have added something to the AST, without modifying the existing nodes

since Oxygen-20120901

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

val add_monotonic_state : State.t -> unit

indicates that the given state (which must depend on Ast.self) is robust against additions to the AST, that is, it will be able to compute information on the new nodes whenever needed. Ast.mark_as_grown will not erase such states, while Ast.mark_as_changed and clearing Ast.self itself will.

since Oxygen-20120901

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

val self : State.t

The state kind associated to the cil AST.

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

val apply_after_computed : (Cil_types.file -> unit) -> unit

Apply the given hook just after building the AST.

since Oxygen-20120901

Internals

Functions below should not be called by casual users.

val is_def_or_last_decl : Cil_types.global -> bool

true if the global is the last one in the AST to introduce a given variable. Used by visitor and printer to relate funspec with appropriate global, and the GUI to remove redundant declarations of globals.

Complexity: O(nb of globals) for the first call, then O(1).

since Oxygen-20120901

val def_or_last_decl : Cil_types.varinfo -> Cil_types.global

def_or_last_decl v returns the global g declaring or defining g such that is_def_or_last_decl g is true.

v must be a global variable declared in the AST.

since Aluminium-20160501

val clear_last_decl : unit -> unit

reset the mapping between a varinfo and the last global introducing it.

since Oxygen-20120901

val set_file : Cil_types.file -> unit

val set_default_initialization : (unit -> unit) -> unit

val mark_as_computed : unit -> unit

since Beryllium-20090901

val add_hook_on_update : (unit -> unit) -> unit

Apply the given hook each time the reference to the AST is updated, including on a project switch.

since Fluorine-20130401