[kernel] ACSL Modules

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

[Kernel] Add warning for implicit int

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

[ivette] Add sidePanel in dome/frame

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

[e-acsl] Here inliner: specialise logical functions called with the Here label

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

Logic normalization transforms predicates and terms from the original
code. Currently the assertion string that is shown to the user when the
assertion fails shows these transformed forms. This should not be the
case, as the user cannot understand where they stem from.

Therefore we need to determine the original forms and use them when
generating the assertion strings.

This commit extends the memoization modules in Logic_normalizer to be
bidirectional maps, such that the original form of a term or predicate
can be determined.

Add the code of generated predicates and logic functions as a global
annotation above their declaration in the generated C code.

When attributes were present but not printed, unnecessary parentheses
were still placed. This applies the same solution for array declarations
to function declarations.

This is not detected by Eva because:
"no assigns clause generated for function length because pointers as arguments is not yet supported"

This commit adds a Here inliner to Logic_normalizer, which specialises
labelled logic functions that are called somewhere exclusively with Here
labels.

Render the memoization tables for predicates and terms bidirectional.
This will help improve user feedback messages in the subsequent commits.
We do not want to confront to the user with feedback messages that
contain transformed code, so we need bidirectional memoization tables in
order to determine the original code that we then can show to the user.

[QED/listmap] Fix change function

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

[kernel] Const-fold enum value in ternary ops

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

[e-acsl] fix logic variable escaping its scope

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

[eva] fix pretty-printing of dot graph in traces domain

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

When using an enum in a ternary operator, the value is const-folded
before checking if it evaluates to `true` or `false` so that const-expr
used as enum values are supported.

Andre Maroneze authored 6 months ago and David Bühler committed 6 months ago

Without escaping strings such as variable names, the produced .dot file
might print '\result' as a variable name, which results in '\r' being
stripped. Dot will then show edges such as 'esult<main>'.

Clean Why3 theories

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

[wp] Fix code semantics float typing

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