From dbba93896ca295e758d12f11c88c34abc66b5f8b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 19 Feb 2021 14:12:46 +0100
Subject: [PATCH] [wp] fixed bug on per-behavior dynamic calls
---
src/plugins/wp/tests/wp_plugin/dynamic.i | 2 +-
.../wp/tests/wp_plugin/oracle/dynamic.res.oracle | 11 ++++++++++-
.../tests/wp_plugin/oracle_qualif/dynamic.res.oracle | 1 +
3 files changed, 12 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i
index ccde8d32cf6..b0caa16f3bf 100644
--- a/src/plugins/wp/tests/wp_plugin/dynamic.i
+++ b/src/plugins/wp/tests/wp_plugin/dynamic.i
@@ -61,7 +61,7 @@ int h0(void);
@ assigns X1;
@ ensures X1==1; */
int behavior (int (*p)(void)) {
- //@ calls h1, h2; // Shall not be proved in default behavior (known bug)
+ //@ calls h1, h2; // Shall not be proved in default behavior
return (*p)();
}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index ad37a67830b..ef17fe7f5ad 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -10,8 +10,17 @@
[wp] tests/wp_plugin/dynamic.i:87: Calls h1
[wp] tests/wp_plugin/dynamic.i:100: Calls unreachable_g
[wp:calls] Dynamic call(s): 6.
-[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
[wp] Warning: Missing RTE guards
+[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
+------------------------------------------------------------
+ Function behavior
+------------------------------------------------------------
+
+Goal Call point h1 h2 in 'behavior' at instruction (file tests/wp_plugin/dynamic.i, line 65):
+Assume { (* Heap *) Type: region(p.base) <= 0. }
+Prove: (global(G_h1_61) = p) \/ (global(G_h2_67) = p).
+
+------------------------------------------------------------
------------------------------------------------------------
Function behavior with behavior bhv1
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index e3e408c44c1..54424105728 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -13,6 +13,7 @@
[wp] [Qed] Goal typed_guarded_call_ensures_part2 : Valid
[wp] [Qed] Goal typed_guarded_call_ensures_2_part1 : Valid
[wp] [Qed] Goal typed_guarded_call_ensures_2_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_behavior_call_point_h1_h2_s15 : Unsuccess
[wp] [Qed] Goal typed_behavior_call_point_h1_h2_s15 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_ensures_part1 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_ensures_part2 : Valid
--
GitLab