[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

When translating a function we must ensure that it cannot re-use any
expressions resulting from translating logic variables from its call
site. One might think that this may not occur, since logic variables are
unique. However sometimes the same logic function needs to be translated
twice (with different signatures). In that case there are indeed
indentical logic variables for different C code to be generated, and
re-using that code would be erroneous.

See the pathological example from the previous commit.

This commit fixes this by clearing the map of logic bindings before
translating a function body.

bin/test.sh -c dev fails for this example.
GCC complains that a.out.frama.c:277:13: error: ‘__gen_e_acsl_v_2’ undeclared

The translation doesn't take into account the scenario that the same
logic function needs to be translated twice. This is due to different
call sites requiring different signatures.

The authors of the translation must worked with the assumption that
uniqueness of logic variables is a strong enough guarantee to be able to
reuse the translation of a logic variable can always be re-used.

This is wrong, since the translation of a logic variable can be re-used
within the context of one function translation, but escapes its scope if
it is re-used in another translation of the same function.

[extlib] remove obsolete functions

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

[release] the installation link now targets GitLab

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

[dev] add ocp-indent to dev-setup dependencies

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

Replaces impact and slicing pragmas by ACSL extensions

Closes #1390

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