Feature/ivette/callgraph

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

[Eva] Improves the emission of integer overflow alarms on a/b and a%b

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

[ci] Add Frama-Clang and Minimal to internal plugin tests

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

[ivette] make sure to generate API before install

Closes #1454

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

Also documents that the behavior of a%b depends on the behavior of a/b.

Only emits overflow alarms on [a/b] when [a] may be equal to [min_int] AND
[b] may be equal to [-1]. Also reduces the values of [a] and [b] when possible.

According to the C standard, section 6.5.5 §6:
"If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a;
otherwise, the behavior of both a/b and a%b is undefined."

[e-acsl] fix wrong equality notion used for terms

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

Feature/tests/include deeper tests directories

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

[Ivette] Fixes default view at first launch.

Closes #1412

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

Do not use Obj in binary_cache.ml

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

Guillaume Combette authored 5 months ago and David Bühler committed 5 months ago

The performance impact is small but measurable (about 2% in run time
difference for polarssl and debie1 in open-source-case-studies). That's
the tradeoff for not having to worry about misusing Obj.

[Eva] Fixes high priority / red status on preconditions.

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

Use Dune 3.11 install source tree

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

When an invalid status is emitted for the instance of a precondition at a
callsite, registers as "high priority" the instance as well as the precondition
itself.

[doc] add missing options in man page

Closes #1425

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

[wp] MemBytes memory model

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