From 0b0ea507ce99ed0d59a4cd8db15e3c6122a3b896 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 28 Jan 2021 11:41:48 +0100
Subject: [PATCH] [wp] Fixes default assigns, warn on assigns everything
---
src/plugins/wp/cfgAnnot.ml | 8 ++++++++
src/plugins/wp/cfgCalculus.ml | 5 ++++-
2 files changed, 12 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index deb19048d7f..b982750d8a3 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -228,11 +228,19 @@ let reverse_loop_contract l = {
loop_assigns = List.rev l.loop_assigns ;
}
+let default_assigns stmt l = {
+ l with
+ loop_assigns =
+ if l.loop_assigns <> [] then l.loop_assigns
+ else [WpPropId.mk_loop_any_assigns_info stmt]
+}
+
let get_loop_contract kf stmt : loop_contract =
let labels = NormAtLabels.labels_loop stmt in
let normalize_pred p = NormAtLabels.preproc_annot labels p in
let normalize_annot (i,p) = i, normalize_pred p in
let normalize_assigns w = NormAtLabels.preproc_assigns labels w in
+ default_assigns stmt @@
reverse_loop_contract @@
Annotations.fold_code_annot
begin fun _emitter ca l ->
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 6c491d3f8d7..dc142fc329c 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -143,7 +143,10 @@ struct
let use_assigns env (a : assigns) w =
match a with
| NoAssignsInfo -> assert false
- | AssignsAny ad -> W.use_assigns env.we None ad w
+ | AssignsAny ad ->
+ Wp_parameters.warning ~current:true ~once:true
+ "Missing assigns clause (assigns 'everything' instead)" ;
+ W.use_assigns env.we None ad w
| AssignsLocations(ap,ad) -> W.use_assigns env.we (Some ap) ad w
let prove_assigns env (a : assigns) w =
--
GitLab