[eacsl] Merge several bugfix into Vanadium

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

The previous solution removed the first `TLogic_coerce` of a term in
`term_to_exp`, which would result in errors if several successive
`TLogic_coerce` were in a term. This commit recursively call
`context_sensitive_term_to_exp` on `TLogic_coerce`.

The exceptions coming from the kernel or OCaml fall through so that they
are catched and processed by the Frama-C plug-in system.

A new function `Error.print_not_yet` is added so that `Contract` can
print the "not yet" message without raising an exception and
interrupting its processing.

If `BuiltinLabel` or `FormalLabel` are encountered, raise `not_yet`.

- name
- version

[eacsl] Fix crash when using GMP loop variant

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

[wp] Remove `M_char` chunk

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

Feature/e acsl/refman upgrade vanadium

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

[Documentation] update documentation about default machdep

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

[analysis-scripts] fix tips for recursion in make-wrapper; add test

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

update installation instructions and why3 config command

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