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.

[kernel] Fixes issue 1494

Closes #1494

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

Feature/libc/assigns trace h

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

[libc] add some tests based on manpages

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

Rewriting [Floating_point] module

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

Only changes the rounding mode if needed (if the new rounding mode is different
from the current one).

Maxime Jacquemin authored 1 month ago and David Bühler committed 1 month ago

As the format is not supported for now, we have removed it.
Witnesses are provided to represent the fact that long
floats are encoded as double. The doc is not yet updated.

Also renames round_to_single_precision_float into round_to_single_precision.

Floating_point contains utilitary functions over ocaml float.
Typed_float provides a typed representation of floating-point numbers, which
encodes the format of the represented number.