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 5 years ago and Michele Alberti committed 5 years ago

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.

David Bühler authored 5 years ago and Michele Alberti committed 5 years ago

Do not stop the subdivision if it can reduce the value of a sub-expression
*and* later subdivisions may improve the value of the complete expression
with this reduction.
If no other subdivision is planned, then stop the subdivision if it cannot
improve the value of the complete expression (as before).