[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

[dev] allow bin/test.sh to work with symbolic links

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

When using symbolic links for plug-in directories (e.g. for testing external
plug-ins), the '-L' flag (follow symbolic links) is necessary to avoid a syntax
error in the script.

[libc] minor change to help coreutils parsing

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

[kernel] Cabs2cil: fixes the alignement computation on packed directives.

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

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

- uses the alignment of a field type instead of its size to compute
  the field alignement.
- removes incorrect special case for flexible array members, introduced to
  circumvent a crash when computing their size. As we now use the alignment
  instead of the size, the crash no longer occurs.
- merges the implementation of two similar cases (whether there are aligned
  field attributes or not).

Feature/martin/test/pass all remaining args to dune

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

Various libc improvements for better parsing of code seen in the wild

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