As it is currently unsound.

Relations are represented as [X±Y ∈ ival]. If the [ival] is too large and
represents all possible values from the type of X and Y, then the relation
is meaningless. Do not infer such relations.

Greatly improves the domain performances.

New boolean option -eva-octagons-through-calls to specify whether the octagons
are propagated through function calls.

Ensures that [Domain.filter `Pre] is only used on a set of bases such that
[Domain.relate bases] is included in [bases].

Only if a boolean [debug] is set.

[pretty] only prints the relations inferred by the octagons domain.
The new function [pretty_debug] also prints the intervals inferred by the domain
and the map of related variables.

Makes the join more precise.

[Eva] Retroactively updates the Changelog for Calcium.

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

[wp] fix error message with eta-expansion

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

[qed+wp] fix typo in inductive types for native coq

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

Resolve "[wp] why-3 output of types with constructors"

Closes #694

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

[WP/Doc] Removes native support of Alt-Ergo/Coq

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

Resolve "Location of temporary variables" #714

Closes #714

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

Thibault Martin authored 5 years ago and Virgile Prevosto committed 5 years ago

decl -> loc
Ajout du paramètre loc pour makeFormalVar et makeGlobalVar