Fix ACSL parser failure on valid type expressions in arrays

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

[Ivette] Dome : added a component to display trees + test in sandbox

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

[wp] fix factory ref-usage

Closes #1491

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

- function pointers were not detected correctly
- this resulted in meaningless clause for hypothese

[Eva] Fix interpretation of \from clauses referring to addresses

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

Maxime Jacquemin authored 1 month ago and Virgile Prevosto committed 1 month ago

Fix for issue #1413

[Kernel] Fixes inconsistent AST on inline functions (when not removed by rmtmps).

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

On the definition of an inline function, cabs2cil created a declaration of a
copy of the function, which was not properly registered and led to a failure
of the AST integrity check:
"function <name> is supposed to be defined, but not registered as such."

The copied declaration was unused and removed by Rmtmps in most cases,
thus preventing the failure, unless the inlined function had a specification
or "-keep-unused-functions all" was set.

This commit removes this copied declaration of inline functions.

[kernel] Parsing float return a result type, new parse_exn function

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

[e-acsl] new compilation scheme via intermedia language

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

Resolve "-machdep avec chemin relatif et -load depuis un autre PWD"

Closes #1474

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

Introduce a new compilation scheme where E-ACSL logic terms are
translated to CIL is implemented as a two-stage process.
First, E-ACSL is translated into an intermediate language. Only then in
the second stage the intermediate language is translated into CIL.

The module Interlang specifies the E-ACSL intermediate language type,
along with pretty printing functions. As this language is still subject
to frequent changes, documentation remains scant for the moment.

The module Interlang_gen helps in the creation of Interlang expressions,
and is thus useful for the first stage. The module Interlang_trans
specifies the translation of Interlang expression to CIL and is relevant
for the second stage.
Both modules make heavy use of the RWS monad, defined in the Monad_rws
module. RWS stands for Reader, Writer, State. The RWS monad is a monad
to model computations with side-effects and environments in a purely
functional and type-safe manner.

As the new compilation scheme covers E-ACSL only partially, it fails on
many E-ACSL terms. Therefore we keep for the moment the old
direct-to-CIL compilation scheme, and, whenever the new compilation
scheme fails for a given sub-term raising the Interlang_gen.Not_covered
exception, we fall back on the direct-to-CIL compilation scheme for that
sub-term.

This simplified version is required for the indirect compilation scheme
introduced in the subsequent commit.

When compiling terms that have already been compiled before, as yet
could result in multiple variable occurrences sharing the same EID,
which is not allowed.