[Cabs2cil] avoid more crashes due to large array initializer

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

[Wp] improvement of the generic sequent simplifier

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

[wp] Weaken code assertions verification + move smoke tests

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

- annots order for multiple emitters is unspecified,
- use the order used in the Printer

[Wp] generic sequent simplifier: applies simplify+assume succesively on each terms of a the disjonctive goal

[WP] Review of the sequent decomposition

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

[Wp] generic sequent simplifier: applies simplify+assume succesively on eacterms of a the conjective hypothesis

Fix/andre/configure plugin deps

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

[wp] Multi selection in Tactical

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

[Compliance] fix and add missing POSIX identifiers

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

- not available from GUI for now
- TacClear and TacUnfold adapted

- Rationale: detect RTE fail sooner

- A1 A2 ... : prove A1 -> hyp A1 -> prove A2 -> hyp A2 ...
- Move smoke tests to the end of code assertions

[doc] User manual: updates the default machdep.

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

David Bühler authored 3 years ago and Andre Maroneze committed 3 years ago

And fixes the example of misaligned read.

[eacsl] Preparatory MR for the labels refactor

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

The term corresponding to the logic var introduced is translated without
the logic var in the logic scope.