Merge branch '1198-messages-perdus-informations-manquantes-lors-de-changements-de-vue-pendant-une-analyse' into 'master'

[ivette] Consolidation of states

Closes #1198

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

[Kernel] fix aligned attribute behavior on typedefs

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

[install] allows to use FRAMAC_INSTALLDIR when PREFIX is undefined

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

[analysis-scripts] add type annotations in Python scripts

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

Handle 'malloc(deallocator)' GCC attribute (prevented GCC re-parsing a file produced by Frama-C)

Closes #1140

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

[lint] use Format everywhere; add missing newlines

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

GCC states that the 'aligned' attribute applied to typedefs can lower the
default type alignment (unlike with structs).

[dev] fix typo in Docker makefile

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

Check for frama_c_init_obj attribute in argument of function call.

Closes #1195

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

[install] Changes dev tools management

Closes #1194 and #1196

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

Virgile Prevosto authored 2 years ago and Michele Alberti committed 2 years ago

also make real errors for KO instructions

- Extend checking to more than just left-values.
- Add function in Cil to check only for frama_c_init_obj attribute (as formals
  should not be annotated with frama_c_mutable one).