Correctly compute `sizeof(L"wide string")`

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

[Ivette] add search on Names for properties

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

[wp] refactor prover selection and cleanup tests

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

[ivette] Server logs

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

Resolve "[server] Filepath serializer"

Closes #1322

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

[Eva] In eval_terms, reduces cvalue state by \base_addr(x) == \base_addr(y).

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

[Ivette/WP] Better proof tree navigation

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

[Ivette] add alerts component

Closes #1384

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

[ivette] enhanced tab view

Closes #1376

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

[e-acsl] fix TLS segment start adress and size

Closes #1147

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

For the special pointers stdin, stdout, stderr, and &errno the results
of \pvalid, \pinitialized, \freeable are statically known, so we return
the result directly instead of generating calls to the runtime functions.

This complements the implementation of the same semantics in the runtime
libraries in the previous commit. As the runtime implementation is
sufficient, this commit is an optimisation.

We currently do not optimise logic functions such as \block_length,
\offset, \base_addr, but we do not expect too many occurrences of terms
such as \base_addr(*(&stdin + 9)).

stdin/stdout/stderr/errno not need explicit initialization or
allocation. They are outside of any of the tracked memory segments.
Notably, due to the subsequent commit they are no longer erroneously
inside the TLS segment. Therefore we need to exempt them from the tests
\valid, \valid_read and \initialized. We also need special treatement
for these objects in \offset, \base_addr, \block_length, \freeable.

In this commit this exemption is implemented as a runtime test, as it
cannot be exhaustively implemented statically (see
tests/memory/errno.c). This runtime exemption is sufficient, however we
will in later commits add such static exemptions anyway for easy cases,
as an optimisation that reduces the number of generated assertions.

This commit simplifies and changes the semantics of the (unused)
e_acsl_safe_locations module.

Thierry Margenstern authored 1 year ago and Jan Rochel committed 11 months ago

The TLS segment no longer includes stdin/stdout/stderr/errno on Linux.
These objects are henceforth no longer found in any of the monitored
segments. Thus some tests involving these objects fail now.

Therefore we need special treatment of these objects in the predicates
\valid, \valid_read and \initialized as well as for the logic functions
\block_length, \offset\ and \base_addr.

This is addressed in the subsequent commit.

Fixes #1147

Fixes opam message for Ivette.

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