From 04ba2fe5bf5cb046f2f58eefacfee5c86c526f96 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Fri, 10 Apr 2020 13:20:49 +0200 Subject: [PATCH] [wp] changelog since calcium --- src/plugins/wp/Changelog | 45 ++++++++++++++++++++++++---------------- 1 file changed, 27 insertions(+), 18 deletions(-) diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog index 3329a913f3c..8e42d3b2e3f 100644 --- a/src/plugins/wp/Changelog +++ b/src/plugins/wp/Changelog @@ -20,24 +20,33 @@ # <Prover>: prover ############################################################################### -- WP [2020/03/26] Added support for invalid-pointer predicate -- WP [2020/02/21] Why3 prover version fallback -- WP [2020/02/21] Why3 prover full-names use ':' instead of ',' --* WP [2020/02/20] Fixes handling of LoopCurrent in loop invariants -- WP [2020/02/10] Specify cache mode with FRAMAC_WP_CACHE=<mode> (-wp-cache-env) -- WP [2020/02/10] Update scripts with FRAMAC_WP_SCRIPT=update and -wp-prover script -- WP [2020/02/10] Move frame conditions to Type section for better filtering -- WP [2020/02/10] Extended frame conditions to pointers inside compound -- WP [2020/02/10] Extended frame conditions with global C-types -- WP [2019/17/04] Control splitting with -wp-max-split <n> -- WP [2019/12/04] Added option -wp-run-all-provers -- WP [2019/01/29] Emit a warning when no goal is generated -- Wp [2019/06/04] Checks for inconsistent requires (-wp-smoke-tests) -- TIP [2018/04/03] Create session directory only on demand -- TIP [2018/03/19] Specification of JSON script format -- Wp [2018/03/18] Additional lemma about remainder (mod) -- TIP [2018/03/18] Refactor structure of session directory (remove models) -- Wp [2018/02/18] Additional lemmas about logical shift compositions + - WP [2020/04/10] Full support for Why3 IEEE float library + - WP [2020/04/10] Removed option -wp-check + - WP [2020/04/09] Added smoke tests for dead call (-wp-smoke-dead-call) + - WP [2020/03/23] Added smoke tests for dead code (-wp-smoke-dead-code) + - WP [2020/03/23] Added smoke tests for dead loop (-wp-smoke-dead-loop) + - WP [2020/03/26] Added support for invalid-pointer predicate + - WP [2020/03/04] Fixed scope problem on block outgoing edge + - WP [2020/02/21] Why3 prover version fallback + - WP [2020/02/21] Why3 prover full-names use ':' instead of ',' + - WP [2020/02/20] Fixes handling of LoopCurrent in loop invariants + - WP [2020/02/10] Specify cache mode with FRAMAC_WP_CACHE=<mode> (-wp-cache-env) + - WP [2020/02/10] Update scripts with FRAMAC_WP_SCRIPT=update and -wp-prover script + - WP [2020/02/10] Move frame conditions to Type section for better filtering + - WP [2020/02/10] Extended frame conditions to pointers inside compound + - WP [2020/02/10] Extended frame conditions with global C-types + - WP [2019/17/04] Control splitting with -wp-max-split <n> + - WP [2019/12/19] Fix drivers in different projects + - WP [2019/12/04] Added option -wp-run-all-provers + - WP [2019/06/04] Checks for inconsistent requires (-wp-smoke-tests) + - WP [2019/01/29] Emit a warning when no goal is generated + - WP [2018/04/17] Limit the number of splits (see -wp-max-split) + - TIP [2018/04/03] Create session directory only on demand + - TIP [2018/03/19] Specification of JSON script format + - WP [2018/03/18] Additional lemma about remainder (mod) + - TIP [2018/03/18] Refactor structure of session directory (remove models) + - TIP [2018/02/20] Extends bitwise tactics to dis-equalities + - WP [2018/02/18] Additional lemmas about logical shift compositions ########################## Plugin WP 20.0 (Calcium) -- GitLab