package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

A cilVisitor (by copy) that simplifies expressions of the type const int x = v, where v is an integer and x is a global variable. Requires a mapping from varinfo to init option (e.g. based on Globals.Vars.find).

  • since Silicon-20161101

the kind of behavior expected for the behavior.

method project : Frama_c_kernel.Project.t option

Project the visitor operates on. Non-nil for copy visitor.

  • since Oxygen-20120901
method plain_copy_visitor : Frama_c_kernel.Cil.cilVisitor

a visitor who only does copies of the nodes according to behavior

visit a whole file.

Invoked for each variable declaration. The children to be traversed are those corresponding to the type and attributes of the variable. Note that variable declarations are GVar, GVarDecl, GFun and GFunDecl globals, the formals of functions prototypes, and the formals and locals of function definitions. This means that the list of formals of a function may be traversed multiple times if there exists both a declaration and a definition, or multiple declarations.

Invoked on each variable use. Here only the SkipChildren and ChangeTo actions make sense since there are no subtrees. Note that the type and attributes of the variable are not traversed for a variable use.

Invoked on each expression occurrence. The subtrees are the subexpressions, the types (for a Cast or SizeOf expression) or the variable use.

Invoked on each lvalue occurrence

Invoked on each offset occurrence that is *not* as part of an initializer list specification, i.e. in an lval or recursively inside an offset.

Invoked on each offset appearing in the list of a CompoundInit initializer.

Invoked on each instruction occurrence. The ChangeTo action can replace this instruction with a list of instructions

Control-flow statement. The default DoChildren action does not create a new statement when the components change. Instead it updates the contents of the original statement. This is done to preserve the sharing with Goto and Case statements that point to the original statement. If you use the ChangeTo action then you should take care of preserving that sharing yourself.

Block.

Function definition. Replaced in place.

Global (vars, types, etc.)

Initializers. Pass the global where this occurs, and the offset

local initializer. pass the variable under initialization.

Use of some type. For typedef, struct, union and enum, the visit is done once at the global defining the type. Thus, children of TComp, TEnum and TNamed are not visited again.

declaration of a struct/union

declaration of an enumeration

visit the declaration of a field of a structure or union

visit the declaration of an enumeration item

Attribute. Each attribute can be replaced by a list

Attribute parameters.

method queueInstr : Frama_c_kernel.Cil_types.instr list -> unit

Add here instructions while visiting to queue them to precede the current statement being processed. Use this method only when you are visiting an expression that is inside a function body, or a statement, because otherwise there will no place for the visitor to place your instructions.

method unqueueInstr : unit -> Frama_c_kernel.Cil_types.instr list

Gets the queue of instructions and resets the queue. This is done automatically for you when you visit statements.

method current_stmt : Frama_c_kernel.Cil_types.stmt option

link to the current statement being visited.

NB: for copy visitor, the stmt is the original one (use get_stmt to obtain the corresponding copy)

method current_kinstr : Frama_c_kernel.Cil_types.kinstr

Kstmt stmt when visiting statement stmt, Kglobal when called outside of a statement.

  • since Carbon-20101201
method push_stmt : Frama_c_kernel.Cil_types.stmt -> unit
method pop_stmt : Frama_c_kernel.Cil_types.stmt -> unit
method current_func : Frama_c_kernel.Cil_types.fundec option

link to the current function being visited.

NB: for copy visitors, the fundec is the original one.

method set_current_func : Frama_c_kernel.Cil_types.fundec -> unit
method reset_current_func : unit -> unit
  • since Oxygen-20120901
  • since Oxygen-20120901
  • since Oxygen-20120901
method fill_global_tables : unit

fill the global environment tables at the end of a full copy in a new project.

method get_filling_actions : (unit -> unit) Stdlib.Queue.t

get the queue of actions to be performed at the end of a full copy.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct