[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

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

David Bühler authored 11 months ago and Allan Blanchard committed 6 months ago

As slice pragmas have been replaced by ACSL extensions.

David Bühler authored 11 months ago and Allan Blanchard committed 6 months ago

As slice pragmas have been replaced by slice ACSL extensions.

David Bühler authored 11 months ago and Allan Blanchard committed 6 months ago

Updates logic_deps to take these directives into account.
Updates pdg and slicing.

David Bühler authored 11 months ago and Allan Blanchard committed 6 months ago

-impact-pragma remains as an invisible deprecated alias of -impact-annot.

Generate Ivette API on the fly

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

Multiple fixes and improvements on CI

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

[wp] -wp-par defaults to number of logical cores

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

[ivette] Graph : replace cycle option by a function

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