From 318d40e4dc281746b6d75183b7b8a87bae6bbb39 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 11 Jun 2021 12:44:35 +0200
Subject: [PATCH] [Changelog] experimental support of "terminates" clauses by
WP
---
src/plugins/wp/Changelog | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 67df94638e1..28cbc17974c 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,14 @@
Plugin WP <next-release>
#########################
+- WP [2021-06-11] Adds an experimental support of "terminates" clauses.
+ Adds the options -wp-declaration-terminate and
+ -wp-frama-c-stdlib to claims that external functions
+ terminates.
+ Adds -wp-declarations-terminate option to claims that
+ defined function terminates.
+ Adds -wp-variant-with-terminates to verify loop
+ variants under the termination hypothesis.
- WP [2021-06-01] -wp-smoke-tests detects incoherent assumes when no
requires are specified, can be disabled with new
option -wp-smoke-dead-assumes
--
GitLab