[Doc/Rte] remove mentions to -rte-no-all and fix table

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

Bugfix/in precedence

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

[kernel] more aggressive constfolding for array dimensions

Closes #651

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

Hence, use a single level for both, especially as we are dealing with obsolete
constructions here.

A ternary operator is a ternary operator. It doesn't matter whether it is
in term or predicate position

also small refactoring of `term_node` method

No parentheses were placed around x or s, regardless of the form of the
subterms and priorities.

See !2285 for information

[Eva] Compiles examples when building the user manual

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

fixes generation of destructors calls in presence of goto

Closes #663 and #501

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

`Kernel_function.is_between s s' s` should return `false` whatever s' is

In presence of objects with destructors, you have to ensure that you won't
bypass object creations in the main block

Fixes for ocaml 4.08

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

[Eva] Supports builtin logical float operators eq_float, le_float, etc

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

And minor changes to the test file.

[coq-wp] Fix syntax error in Vlist.v

Closes #666

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

These operators are eq_float, ne_float, lt_float, le_float, gt_float, gt_float.
And respectively for the double type.

Required to compare infinite and NaN which do not exist in the real type.

As we want to use the latter in the former.

Fixes #651

use why3 api

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