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).

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

If an interval contains positive and negative floating-point values, cuts the
interval at 0. Otherwise, uses the same strategy as before: cuts the interval
at the mathematical average of its bounds.

This strategy always reaches the maximal precision in one split on e*e squares,
which is the most common pattern for subdivisions.
In the tests, it decreases the precision on computations of e-e, where a split
at 0 is useless. However, this is not a common pattern in real codes.

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

Previous commits have introduced the new runs (and oracles) without this option.
This commit only contains the changes due to this option:
- no alarms for non-finite floating-point values.
- in the function [around_zeros], no reduction of the variable [f] as the
  division by 0 simply computes ∞.
- volatile floating-point variables have a value in [-∞..∞] ∪ NaN.

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

The next commit changes the new runs to use the option -warn-special-float none.
This commit is introduced to better highlight the changes due to this option
in the next commit.

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

This commit is separated from the next to avoid mixing up the oracle moves with
the addition of new oracles for the new runs.

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

This commit is separated from the next to avoid mixing up the oracle moves with
the addition of new oracles for the new runs.

[RENAME PLUGIN] Builtin -> Instantiate

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

[wp] import nupw 6.6

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

more robust definition of space for frama-c.mk

Closes #809

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

[wp] prover name fallback

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

Supports ghost-else contruct

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

The cache makes the tests deterministic

Feature/server/gui

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

[Eva] Small changes in the abstract domain signature.

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

In the function [initialize_variable_using_type].
Adds a constructor [Return] to [variable_kind] for the special variable that
stores the return value of a function call.