From e84077d56dfe7f781a68089d5b2f0109a2b9ea85 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 29 Jan 2019 09:16:07 +0100
Subject: [PATCH] [wp] known bug in absence of default bhv
---
src/plugins/wp/tests/wp_plugin/dynamic.i | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i
index 3f9e7b87a8b..ccde8d32cf6 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;
+ //@ calls h1, h2; // Shall not be proved in default behavior (known bug)
return (*p)();
}
--
GitLab