From 1c45a4c9247458b523601e400e8bcda42a428188 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 10 Mar 2021 15:31:30 +0100
Subject: [PATCH] [wp] Fix assigns labels for called functions
---
src/plugins/wp/cfgAnnot.ml | 6 +++++-
src/plugins/wp/tests/wp_acsl/old-assigns.c | 12 ++++++++++++
.../wp_acsl/oracle/old-assigns.res.oracle | 19 +++++++++++++++++++
.../oracle_qualif/old-assigns.res.oracle | 13 +++++++++++++
4 files changed, 49 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/wp/tests/wp_acsl/old-assigns.c
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/old-assigns.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/old-assigns.res.oracle
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index c837a3ede6b..f67f603fc98 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -247,13 +247,17 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
List.iter (add wpost @@ mk_post Normal) bhv.b_post_cond ;
List.iter (add wexit @@ mk_post Exits) bhv.b_post_cond ;
end behaviors ;
+ let assigns = match assigns_upper_bound behaviors with
+ | WritesAny -> WritesAny
+ | Writes froms -> Writes (normalize_froms Normal froms)
+ in
{
contract_cond = List.rev !wcond ;
contract_hpre = List.rev !whpre ;
contract_post = List.rev !wpost ;
contract_exit = List.rev !wexit ;
contract_smoke = [] ;
- contract_assigns = assigns_upper_bound behaviors
+ contract_assigns = assigns
}
end)
diff --git a/src/plugins/wp/tests/wp_acsl/old-assigns.c b/src/plugins/wp/tests/wp_acsl/old-assigns.c
new file mode 100644
index 00000000000..d15399639e4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/old-assigns.c
@@ -0,0 +1,12 @@
+#include <string.h>
+
+/*@ assigns dest[0..strlen{Old}(src)]; @*/
+void strcpy_OLD(char *restrict dest, const char *restrict src);
+
+/*@
+ requires \separated(dest+(0..), src+(0..));
+ assigns dest[0..strlen(src)];
+*/
+void old(char *dest, const char *src) {
+ strcpy_OLD(dest, src);
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/old-assigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/old-assigns.res.oracle
new file mode 100644
index 00000000000..568225a6abd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/old-assigns.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/old-assigns.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function old
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/old-assigns.c, line 8) in 'old':
+Call Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/old-assigns.c, line 8) in 'old':
+Call Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/old-assigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/old-assigns.res.oracle
new file mode 100644
index 00000000000..9d6f2033859
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/old-assigns.res.oracle
@@ -0,0 +1,13 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/old-assigns.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Qed] Goal typed_old_assigns_exit : Valid
+[wp] [Qed] Goal typed_old_assigns_normal : Valid
+[wp] Proved goals: 2 / 2
+ Qed: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ old 2 - 2 100%
+------------------------------------------------------------
--
GitLab