- it works only when the function is unique currently
- only used for tests

an antediluvian comment hinted at some weird behavior of gcc and
MSVC at that time, but gcc is now fully ISO compliant in this respect
Waiting for complaints against the MSVC machdep to see whether special
case is warranted there.

Use same pattern as in metrics_acsl.ml.

Keep the APIs of Visitor and Cil.visit* in sync

Aorai does not get in the way anymore

Meddling with mutable fields is not the proper way to do it

David Bühler authored 3 years ago and Virgile Prevosto committed 3 years ago

Skips the visit of C codes.

David Bühler authored 3 years ago and Virgile Prevosto committed 3 years ago

Only visits functions and variables definitions.

David Bühler authored 3 years ago and Virgile Prevosto committed 3 years ago

Only visits function and variable definitions.

David Bühler authored 3 years ago and Virgile Prevosto committed 3 years ago

Only processes function specifications.
Does not use a visitor anymore.

David Bühler authored 3 years ago and Virgile Prevosto committed 3 years ago

Only visits globals that are ghost or may contain ghost code.

David Bühler authored 3 years ago and Virgile Prevosto committed 3 years ago

Only visits function definitions: avoids visiting the specifications of the
Frama-C libc.

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.

The final computation state [Computed] or [Aborted] is set by [compute_function],
before calling the function [post_analysis] of domains, as those may use
plugins that use Eva results.