Frama-C API - Ast
Access to the CIL AST which must be used from Frama-C.
May be raised by function get
below.
Might be raised by UntypedFiles.get
below
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.
call this function whenever you've made some changes in place inside the AST
call this function whenever you have added something to the AST, without modifying the existing nodes
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.
val self : State.t
The state kind associated to the cil AST.
val apply_after_computed : (Cil_types.file -> unit) -> unit
Apply the given hook just after building the AST.
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).
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.
reset the mapping between a varinfo and the last global introducing it.
val set_file : Cil_types.file -> unit