[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.

- Replace `Env.with_rte` and `Env.with_params` to be able to set `rte`
and `kinstr` for an environment;
- Remove `kinstr` parameters from the `Contract` function to use the
`kinstr` of the environment instead;
- Setup environment `kinstr` when injecting code into a statement or
when translating code or function annotation.

Regarding `Translate_annots.pre_funspec` and
`Translate_annots.post_funspec`, since they only translate function
annotations, the `kinstr` is directly set to `Kglobal` in the functions
instead of being taken as a parameter.

[eacsl] Ajout du support de la concurrence

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

We use spin locks so as to not require Pthreads.

[kernel] Usable_emitter.get returns [orphan] when the emitter does not exists.

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

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

Instead of raising a [Not_found] exception.
Fixes crashes when loading a Frama-C save when an original emitter is not
available.

[Variadic] add several wkeys

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