package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

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/Visitor/index.html

Module `Frama_c_kernel.Visitor`

Frama-C visitors dealing with projects.

class type frama_c_visitor = object ... end

Class type for a Db-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

class frama_c_inplace : frama_c_visitor

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

class frama_c_copy : Project.t -> frama_c_visitor

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.

class frama_c_refresh : Project.t -> frama_c_visitor

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

class generic_frama_c_visitor : Visitor_behavior.t -> frama_c_visitor

Generic class that abstracts over frama_c_inplace and frama_c_copy.

val visitFramacFileCopy : frama_c_visitor -> Cil_types.file -> Cil_types.file

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.

val visitFramacFile : frama_c_visitor -> Cil_types.file -> unit

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.

val visitFramacFileSameGlobals : frama_c_visitor -> Cil_types.file -> unit

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
Plug-in Development Guide

val visitFramacFileFunctions : frama_c_visitor -> Cil_types.file -> unit

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

val visitFramacGlobal : 
  frama_c_visitor ->
  Cil_types.global ->
  Cil_types.global list

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.

val visitFramacKf : frama_c_visitor -> Kernel_function.t -> Kernel_function.t

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

val visitFramacFunction : 
  frama_c_visitor ->
  Cil_types.fundec ->
  Cil_types.fundec

Visit a function definition.

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

val visitFramacExpr : frama_c_visitor -> Cil_types.exp -> Cil_types.exp

Visit an expression

val visitFramacLval : frama_c_visitor -> Cil_types.lval -> Cil_types.lval

Visit an lvalue

val visitFramacOffset : frama_c_visitor -> Cil_types.offset -> Cil_types.offset

Visit an lvalue or recursive offset

val visitFramacInitOffset : 
  frama_c_visitor ->
  Cil_types.offset ->
  Cil_types.offset

Visit an initializer offset

val visitFramacInstr : 
  frama_c_visitor ->
  Cil_types.instr ->
  Cil_types.instr list

Visit an instruction

val visitFramacStmt : frama_c_visitor -> Cil_types.stmt -> Cil_types.stmt

Visit a statement

val visitFramacBlock : frama_c_visitor -> Cil_types.block -> Cil_types.block

Visit a block

val visitFramacType : frama_c_visitor -> Cil_types.typ -> Cil_types.typ

Visit a type

val visitFramacVarDecl : 
  frama_c_visitor ->
  Cil_types.varinfo ->
  Cil_types.varinfo

Visit a variable declaration

val visitFramacLogicVarDecl : 
  frama_c_visitor ->
  Cil_types.logic_var ->
  Cil_types.logic_var

Visit a logic variable declaration

since Magnesium-20151001

val visitFramacInit : 
  frama_c_visitor ->
  Cil_types.varinfo ->
  Cil_types.offset ->
  Cil_types.init ->
  Cil_types.init

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

val visitFramacAttributes : 
  frama_c_visitor ->
  Cil_types.attribute list ->
  Cil_types.attribute list

Visit a list of attributes

val visitFramacAnnotation : 
  frama_c_visitor ->
  Cil_types.global_annotation ->
  Cil_types.global_annotation

val visitFramacCodeAnnotation : 
  frama_c_visitor ->
  Cil_types.code_annotation ->
  Cil_types.code_annotation

val visitFramacAllocation : 
  frama_c_visitor ->
  Cil_types.allocation ->
  Cil_types.allocation

val visitFramacAssigns : 
  frama_c_visitor ->
  Cil_types.assigns ->
  Cil_types.assigns

val visitFramacFrom : frama_c_visitor -> Cil_types.from -> Cil_types.from

val visitFramacDeps : frama_c_visitor -> Cil_types.deps -> Cil_types.deps

val visitFramacFunspec : 
  frama_c_visitor ->
  Cil_types.funspec ->
  Cil_types.funspec

val visitFramacLogicType : 
  frama_c_visitor ->
  Cil_types.logic_type ->
  Cil_types.logic_type

val visitFramacPredicateNode : 
  frama_c_visitor ->
  Cil_types.predicate_node ->
  Cil_types.predicate_node

val visitFramacPredicate : 
  frama_c_visitor ->
  Cil_types.predicate ->
  Cil_types.predicate

val visitFramacIdPredicate : 
  frama_c_visitor ->
  Cil_types.identified_predicate ->
  Cil_types.identified_predicate

val visitFramacPredicates : 
  frama_c_visitor ->
  Cil_types.identified_predicate list ->
  Cil_types.identified_predicate list

val visitFramacIdTerm : 
  frama_c_visitor ->
  Cil_types.identified_term ->
  Cil_types.identified_term

visit identified_term.

since Oxygen-20120901

val visitFramacTerm : frama_c_visitor -> Cil_types.term -> Cil_types.term

val visitFramacTermLval : 
  frama_c_visitor ->
  Cil_types.term_lval ->
  Cil_types.term_lval

val visitFramacTermLhost : 
  frama_c_visitor ->
  Cil_types.term_lhost ->
  Cil_types.term_lhost

val visitFramacTermOffset : 
  frama_c_visitor ->
  Cil_types.term_offset ->
  Cil_types.term_offset

val visitFramacLogicInfo : 
  frama_c_visitor ->
  Cil_types.logic_info ->
  Cil_types.logic_info

val visitFramacBehavior : 
  frama_c_visitor ->
  Cil_types.funbehavior ->
  Cil_types.funbehavior

val visitFramacBehaviors : 
  frama_c_visitor ->
  Cil_types.funbehavior list ->
  Cil_types.funbehavior list

val visitFramacModelInfo : 
  frama_c_visitor ->
  Cil_types.model_info ->
  Cil_types.model_info

val visitFramacExtended : 
  frama_c_visitor ->
  Cil_types.acsl_extension ->
  Cil_types.acsl_extension