module Ast:sig..end
Access to the CIL AST which must be used from Frama-C.
exception Bad_Initialization of string
May be raised by function Ast.get below.
exception NoUntypedAst
Might be raised by Ast.UntypedFiles.get below
module UntypedFiles:sig..end
val get : unit -> Cil_types.fileGet the cil file representation.
One of the initialization function of module File has to be called
before using this function.
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 compute : unit -> unitEnforce the computation of the AST.
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 -> boolval mark_as_changed : unit -> unitcall this function whenever you've made some changes in place inside the AST
val mark_as_grown : unit -> unitcall this function whenever you have added something to the AST, without modifying the existing nodes
val add_monotonic_state : State.t -> unitindicates 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.tThe state kind associated to the cil AST.
val apply_after_computed : (Cil_types.file -> unit) -> unitApply the given hook just after building the AST.
Functions below should not be called by casual users.
val is_def_or_last_decl : Cil_types.global -> booltrue 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.globaldef_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.
val clear_last_decl : unit -> unitreset the mapping between a varinfo and the last global introducing it.
val set_file : Cil_types.file -> unit
val set_default_initialization : (unit -> unit) -> unit
val mark_as_computed : unit -> unitval add_hook_on_update : (unit -> unit) -> unitApply the given hook each time the reference to the AST is updated, including on a project switch.