The `__eacsl_globals_clean()` global function is only created if there
are globals variables. A `return;` statement is added at the end of the
function to satisfy Frama-C invariants.

The `e-acsl-gcc.sh` only looked for the Frama-C executable in the
`$PATH`. This commit updates the search for Frama-C to be able
to detect the binary if installed in a folder not added to the path,
or if running the script from the development sources.

Informs the domain that the current evaluation is a subdivision of the complete
evaluation.
Evaluation engine: [root] is set to false for subdivided evaluations.

The context currently contains the fields:
- root: is the queried expression the root expression being evaluated, or is it
  a subexpression?
- sudivision: the maximum number of subdivisions for the current evaluation.
- subdivided: is the evaluation being subdivided?

[root] is always set to false for subdivided evaluations.

The abstract domain queries [extract_expr] and [extract_lval] have a new
boolean parameter [root], which is true for the root expression being
evaluated, and false for all its sub-expression and lvalues.

The contracts are updated to mention the behaviors in the contracts of
`stdlib.h` and satisfy Eva.

[eacsl] Merge the specifications from the RTL functions with the corresponding functions from the user's project