Take tentative definitions into account when merging

Closes #1032

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

[eacsl] Add support of `check` annotations

Closes e-acsl#142

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

Use the `predicate_kind` of `toplevel_predicate` to decide if an
assertion should be blocking or not.

The function `Translate.translate_predicate` is meant to translate the
root predicate of an assertion, so it makes sense to use
`toplevel_predicate` as a parameter and it gives access to the
`predicate_kind`.

The loop invariants in `Env` are also stored as `toplevel_predicate`
to facilitate the translation.

[Kernel] add wkey CERT:MSC:37 to existing warning

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

[eacsl] Fix for `Misc.ptr_base`

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

Contrary to the function `Cil.stripCasts`, the function
`Misc.strip_casts` returns the list of removed casts.

Contrary to the function `Cil.mkCast`, the function `Misc.add_casts` is
able to successively add a list of cast like the one returned by
`Misc.strip_casts`.

[wp] Fixes lemma dependencies

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

A tentative def turned into 0-initialization can't be merged with
an explicit definition from another translation unit.

[Ptests] changes to prefigure dune testing mode  (adds EXIT directive)

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

Feature/andre/more filepath options

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