Frama-C API - Visitor

Class type for a database-aware visitor. This is done by defining auxiliary methods that can be redefined in inherited classes, while the corresponding ones from Cil.cilVisitor must retain their values as defined here. Otherwise, annotations may not be visited properly. The replaced functions are

in-place visitor; always act in the current project.

Copying visitor. The Project.t argument specifies in which project the visitor creates the new values. (Technically, the method fill_global_tables is called inside this project.) See File.init_project_from_visitor and create_project_from_visitor for possible uses.

Similar to frama_c_copy, but ids will be refreshed in the copy.

Generic class that abstracts over frama_c_inplace and frama_c_copy.

Visit a file. This will re-cons all globals TWICE (so that it is tail-recursive). Use Cil.visitCilFileSameGlobals if your visitor will not change the list of globals.

Same thing, but the result is ignored. The given visitor must thus be an inplace visitor. Nothing is done if the visitor is a copy visitor.

A visitor for the whole file that does not change the globals (but maybe changes things inside the globals). Use this function instead of Visitor.visitFramacFile whenever appropriate because it is more efficient for long files.

• see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Visit all function definitions of a file. Use this function instead of Visitor.visitFramacFile or Visitor.visitFramacFileSameGlobals if your visitor only needs function bodies to avoid visiting other globals, including libc functions and their specifications.

• since 25.0-Manganese

Visit a global.

Warning Do not call this function during another visit using the same visitor, as it is not reentrant: the inner visit will leave the visitor in an inconsistent state for the outer visit.

Visit a kernel_function. More precisely, the entry point for the visit will be the global corresponding to the last declaration/definition of the kf. The returned kf is the one that has the varinfo associated to the varinfo of the original kf. If this is a new kf, it is however the responsibility of the visitor to insert it in the AST at the appropriate place.

• since Aluminium-20160501

Visit a function definition.

• see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Visit an expression

Visit an lvalue

Visit an lvalue or recursive offset

Visit an initializer offset

Visit an instruction

Visit a statement

Visit a block

Visit a type

Visit a variable declaration

Visit a logic variable declaration

• since Magnesium-20151001

Visit an initializer, pass also the global to which this belongs and the offset.

Visit a list of attributes

visit identified_term.

• since Oxygen-20120901