David Bühler authored 4 years ago and Loïc Correnson committed 4 years ago

The behaviors leading to forbidden floating-point values are now removed, and
the negation of their assumes are added as preconditions.

Fixes #877.

Nowadays, Metrics has option -metrics-no-libc to exclude definitions from
the Frama-C standard library, which was the purpose of the __FRAMA_C_MODEL__.
Also, several libc variables were lacking the attribute, leading to
inconsistent results.

This check will only be fully operational when rmtmps becomes optional,
but it still protects against errors in used definitions.

Fixes issue #614