package frama-c

  1. Overview
  2. Docs
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

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. N
    Nicolas Bellec
  6. T
    Thibaut Benjamin
  7. A
    Allan Blanchard
  8. L
    Lionel Blatter
  9. F
    François Bobot
  10. R
    Richard Bonichon
  11. V
    Vincent Botbol
  12. Q
    Quentin Bouillaguet
  13. D
    David Bühler
  14. Z
    Zakaria Chihani
  15. L
    Loïc Correnson
  16. J
    Julien Crétin
  17. P
    Pascal Cuoq
  18. Z
    Zaynah Dargaye
  19. B
    Basile Desloges
  20. J
    Jean-Christophe Filliâtre
  21. P
    Philippe Herrmann
  22. M
    Maxime Jacquemin
  23. F
    Florent Kirchner
  24. A
    Alexander Kogtenkov
  25. R
    Remi Lazarini
  26. T
    Tristan Le Gall
  27. J
    Jean-Christophe Léchenet
  28. M
    Matthieu Lemerre
  29. D
    Dara Ly
  30. D
    David Maison
  31. C
    Claude Marché
  32. A
    André Maroneze
  33. T
    Thibault Martin
  34. F
    Fonenantsoa Maurica
  35. M
    Melody Méaulle
  36. B
    Benjamin Monate
  37. Y
    Yannick Moy
  38. P
    Pierre Nigron
  39. A
    Anne Pacalet
  40. V
    Valentin Perrelle
  41. G
    Guillaume Petiot
  42. D
    Dario Pinto
  43. V
    Virgile Prevosto
  44. A
    Armand Puccetti
  45. F
    Félix Ridoux
  46. V
    Virgile Robles
  47. J
    Jan Rochel
  48. M
    Muriel Roger
  49. J
    Julien Signoles
  50. N
    Nicolas Stouls
  51. K
    Kostyantyn Vorobyov
  52. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Cil/class-nopCilVisitor/index.html

Class Cil.nopCilVisitor

Default in place visitor doing nothing and operating on current project.

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 : 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) Queue.t

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