Merge branch '1212-ivette-update-astview-when-alarms-are-emitted-or-statements-are-marked-as-dead' into 'master'

Resolve "[ivette] Update ASTview when alarms are emitted or statements are marked as dead"

Closes #1212

See merge request frama-c/frama-c!4154

Loïc Correnson authored 1 year ago and Allan Blanchard committed 1 year ago

This reverts commit 0bd1d1f0c17fb811469aa8b57fb4bd8f4acbc83b.

[ci] force keys update

See merge request frama-c/frama-c!4183

Fix/wp/double assumes normalization

See merge request frama-c/frama-c!4181

[Eva] User manual: updates section about the octagon domain.

See merge request frama-c/frama-c!4180

[ci] add pathcrawler

See merge request frama-c/frama-c!4179

Retroactively updates the Changelog for Eva and Ivette.

See merge request frama-c/frama-c!4175

- MR !4164: fixes interpretation of Eva annotations.
- MR !3993: allows comments in .ya automata files and specifications about
  floating-point variables. Also, Eva shows the name of enumeration tags
  instead of their integer values.
- MR !4147: ivette shows the status of uninitialized and escaping variables.
- MR !4151: better display of large integer sets.
- MR !4134: the values table can show the status of ACSL predicates, the values
  of C lvalues in these predicates, and the values of function parameters.
- MR !4098: fixes a soundness bug of the equality domain.
- MR !4065: fixes performances issues on programs with too many callsites.
- MR !4015: fixes the bitwise domain on big-endian architecture.
- MR !4046: better partitioning splits on ACSL predicates.

[Eva] octagons: octagons about pointers

See merge request frama-c/frama-c!4032

Uses faster but approximating functions for [join], [narrow] and [add]:
in resulting maps (m, i), the inverse map [i] may contain variables that do
not appear in [m]. Do not fail when this is the case.

Fixes performance issues: the initialization of large arrays or structures
can lead to a very large number of relations or intervals.

Also, do not infer intervals on volatile lvalues.