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.

use why3 api

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

Fixes relative order of defined and declared variables

Closes #653

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

For compatibility with ocaml 4.08.

For compatibility with ocaml 4.08.

Virgile Prevosto authored 5 years ago and David Bühler committed 5 years ago

If a defined local is referenced to in the type of a declared one (e.g. in
a `sizeof` expression as part of an array length), the `Local_init` will put
its actual definition after the declaration (which occurs at the beginning of
the block, resulting in at least pretty-printing unparsable code. We generate
undeclared temp variables of the same type to overcome the issue, like in
bb30d0e4

Virgile Prevosto authored 5 years ago and David Bühler committed 5 years ago

they can appear before their `Local_init`, e.g. in a `SizeOfE` in the
size expression of a local array. Furthermore, we weren't really checking that
declared locals weren't used before the block in which they were supposed to
appear.

Virgile Prevosto authored 5 years ago and David Bühler committed 5 years ago

from a dependency point of view, this make more sense.

[Libc] add specs for chdir/chroot

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

[wp] Improves simplifiers

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

[configure] show version of found libraries

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

Bugfix/issue549

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

Resolve "[WP/QED] Incorrect transformations with binders"

Closes #654

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