diff --git a/Changelog b/Changelog index 65f7db922aecdc1a77d11359a81e8627262b66f4..8c9a705d3c372b62fee986ca97d723c021c62eec 100644 --- a/Changelog +++ b/Changelog @@ -17,6 +17,12 @@ Open Source Release <next-release> ################################## +- Eva [2019/10/21] New octagon domain inferring relations of the form + l ≤ ±X±Y ≤ e between pairs of integer variables X and Y. Enabled + with option -eva-octagon-domain. Only infers relations between + pairs of scalar variables occuring in a same instruction. + Intra-procedural by default; octagons can be propagated through + function calls with option -eva-octagon-through-calls. - Eva [2019/10/04] Evaluates ACSL predicates \is_plus_infinity and \is_minus_infinity. - Kernel [2019/10/04] Supports macro INFINITY and NAN.