also impose replay mode in the CI, so as to be warned if cache needs updating.

can be useful when something fails even though we don't necessarily
want it in oracles.

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

Use same pattern as in metrics_acsl.ml.

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

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.