otherwise, we might end up with an improper crash of cabs2cil

Actually we can't completely avoid typing the branch that won't be evaluated:
we need its type in order to convert the value of the other branch if needed.

apart from overflowing float-to-int conversions, they're not really useful

also minor refactoring of smart constructor for float constants

More or less needed if you want to use dynamically loaded plug-ins, for which
dependency tracking becomes more complicated.

[Headers] cleanning header spec file

Closes #816

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

This reverts commit 7dc7e69e.

[headers] cleaning header spec file

Closes #816

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

[ACSL] replace (T[size])(ptr) by *((T(*)[size])(ptr))

Closes #780

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

[Eva] evaluate logic function memchr_off

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

Only export them for the logic evalution by the cvalue domain.

It seems not really deterministic

This reverts commit 596ed001.

[Eva] Adjusts the strategy to subdivide floating-point intervals

Closes Value/Value#128

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

David Bühler authored Mar 02, 2020 and Michele Alberti committed Mar 02, 2020

When the subdivision on a sub-expression [s] is performed according to [s] and
not according to the complete expression [e], we then reevaluate [e] with the
result of the subdivision. However, the valuation should be cleared before.
Otherwise, the reevaluation uses the cache and not the reduced values computed
by the subdivision.