From 84aee1b20f8b5a7da7a4bb24e17972a3342f44ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Mon, 21 Oct 2019 10:46:48 +0200 Subject: [PATCH] [Eva] Adds a Changelog entry for the octagon domain. --- Changelog | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Changelog b/Changelog index 65f7db922ae..8c9a705d3c3 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. -- GitLab