src/kernel_internals/typing/asm_contracts.ml · b521f5d723b6f46043b0ddbb95dbc36d0952ab70 · pub / frama-c

3 years ago

[kernel] Visitor: adds a function to visit all function definitions of a file. · b521f5d7

David Bühler authored 3 years ago and

Virgile Prevosto committed 3 years ago

For visitors that only need function C bodies, replaces uses of
[visitFramacFileSameGlobals], which visits all globals of a file, by
[visitFramacFileFunctions], which visits only function definitions.

Also optimizes these visitors by skipping the visit of some nodes,
especially the visit of functions specifications and code annotations.

b521f5d7

History

[kernel] Visitor: adds a function to visit all function definitions of a file.

David Bühler authored 3 years ago and

Virgile Prevosto committed 3 years ago

For visitors that only need function C bodies, replaces uses of
[visitFramacFileSameGlobals], which visits all globals of a file, by
[visitFramacFileFunctions], which visits only function definitions.

Also optimizes these visitors by skipping the visit of some nodes,
especially the visit of functions specifications and code annotations.