From aae47aab578594d76aba2f1a2a685eea2d642a18 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 12 Oct 2020 14:13:20 +0200
Subject: [PATCH] [wp] More robust hypotheses behaviors
---
src/plugins/wp/MemoryContext.ml | 2 +-
.../wp_acsl/oracle/assigns_path.res.oracle | 2 +-
.../wp_acsl/oracle/chunk_typing.res.oracle | 2 +-
.../wp_acsl/oracle/funvar_inv.0.res.oracle | 6 +++---
.../tests/wp_acsl/oracle/pointer.res.oracle | 4 ++--
.../oracle_qualif/assigns_path.res.oracle | 2 +-
.../oracle_qualif/chunk_typing.res.oracle | 2 +-
.../oracle_qualif/pointer.0.res.oracle | 2 +-
.../oracle_qualif/pointer.1.res.oracle | 2 +-
.../wp/tests/wp_bts/oracle/bts0843.res.oracle | 2 +-
.../tests/wp_bts/oracle/bts_1828.0.res.oracle | 2 +-
.../tests/wp_bts/oracle/bts_1828.1.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts0843.res.oracle | 2 +-
.../oracle_qualif/bts_1828.0.res.oracle | 2 +-
.../oracle_qualif/bts_1828.1.res.oracle | 2 +-
.../oracle/frama_c_exo3_solved.old.res.oracle | 2 +-
.../frama_c_exo3_solved.old.v2.res.oracle | 2 +-
.../frama_c_exo3_solved.old.res.oracle | 2 +-
.../frama_c_exo3_solved.old.v2.res.oracle | 2 +-
.../alias_assigns_hypotheses.0.res.oracle | 18 ++++++++---------
.../alias_assigns_hypotheses.1.res.oracle | 18 ++++++++---------
.../alias_escapes_hypotheses.res.oracle | 8 ++++----
.../tests/wp_hoare/oracle/byref.1.res.oracle | 6 +++---
.../wp_hoare/oracle/dispatch_var.res.oracle | 12 +++++------
.../oracle/dispatch_var2.0.res.oracle | 8 ++++----
.../oracle/dispatch_var2.1.res.oracle | 8 ++++----
.../wp_hoare/oracle/reference.res.oracle | 10 +++++-----
.../oracle/reference_and_struct.res.oracle | 6 +++---
.../oracle/reference_array.res.oracle | 8 ++++----
.../oracle/reference_array_simple.res.oracle | 2 +-
.../wp_hoare/oracle/refguards.res.oracle | 6 +++---
.../alias_assigns_hypotheses.res.oracle | 18 ++++++++---------
.../wp_hoare/oracle_qualif/byref.1.res.oracle | 6 +++---
.../oracle_qualif/dispatch_var.res.oracle | 12 +++++------
.../oracle_qualif/dispatch_var2.0.res.oracle | 8 ++++----
.../oracle_qualif/dispatch_var2.1.res.oracle | 8 ++++----
.../oracle_qualif/reference.res.oracle | 10 +++++-----
.../reference_and_struct.res.oracle | 6 +++---
.../oracle_qualif/reference_array.res.oracle | 8 ++++----
.../reference_array_simple.res.oracle | 2 +-
.../oracle_qualif/refguards.res.oracle | 6 +++---
.../tests/wp_plugin/oracle/dynamic.res.oracle | 8 ++++----
.../wp_plugin/oracle/overassign.res.oracle | 4 ++--
.../wp_plugin/oracle/post_assigns.res.oracle | 2 +-
.../wp/tests/wp_plugin/oracle/sep.res.oracle | 20 ++++++++++---------
.../wp_plugin/oracle/subset_fopen.res.oracle | 2 +-
.../wp_plugin/oracle/volatile.0.res.oracle | 2 +-
.../wp_plugin/oracle/volatile.1.res.oracle | 2 +-
.../oracle_qualif/dynamic.res.oracle | 8 ++++----
.../oracle_qualif/overassign.res.oracle | 4 ++--
.../oracle_qualif/post_assigns.res.oracle | 2 +-
.../oracle_qualif/subset_fopen.res.oracle | 2 +-
.../wp_tip/oracle/chunk_printing.res.oracle | 4 ++--
.../tests/wp_typed/oracle/mvar.0.res.oracle | 2 +-
.../tests/wp_typed/oracle/mvar.1.res.oracle | 2 +-
.../wp_typed/oracle/unit_alloc.0.res.oracle | 2 +-
.../wp_typed/oracle/unit_alloc.1.res.oracle | 2 +-
.../wp_typed/oracle/unit_ite.1.res.oracle | 2 +-
.../wp_typed/oracle/unit_labels.1.res.oracle | 2 +-
.../oracle/unit_loopscope.1.res.oracle | 2 +-
.../wp_typed/oracle/user_injector.res.oracle | 2 +-
.../wp_typed/oracle/user_swap.1.res.oracle | 2 +-
.../wp_typed/oracle_qualif/mvar.res.oracle | 2 +-
.../oracle_qualif/unit_alloc.0.res.oracle | 2 +-
.../oracle_qualif/unit_alloc.1.res.oracle | 2 +-
.../oracle_qualif/unit_loopscope.1.res.oracle | 2 +-
.../oracle_qualif/user_injector.0.res.oracle | 2 +-
.../oracle_qualif/user_injector.1.res.oracle | 2 +-
.../oracle_qualif/user_swap.1.res.oracle | 2 +-
.../tests/wp_usage/oracle/caveat.1.res.oracle | 6 +++---
.../tests/wp_usage/oracle/caveat2.res.oracle | 2 +-
.../wp_usage/oracle/caveat_range.res.oracle | 2 +-
.../tests/wp_usage/oracle/global.1.res.oracle | 2 +-
.../tests/wp_usage/oracle/global.2.res.oracle | 8 +++++---
.../oracle/issue-189-bis.1.res.oracle | 2 +-
.../wp_usage/oracle/issue-189.2.res.oracle | 2 +-
.../oracle/ref-usage-lemmas.res.oracle | 2 +-
.../wp_usage/oracle_qualif/caveat2.res.oracle | 2 +-
.../oracle_qualif/caveat_range.res.oracle | 2 +-
.../oracle_qualif/issue-189-bis.1.res.oracle | 2 +-
80 files changed, 183 insertions(+), 179 deletions(-)
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 5ad6dcba154..b142d6f84c5 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -357,7 +357,7 @@ let compute_behavior kf name hypotheses_computer =
| [], [] -> None
| reqs, ens ->
Some {
- b_name = name ;
+ b_name = Annotations.fresh_behavior_name kf ("wp_" ^ name) ;
b_requires = reqs ;
b_assumes = [] ;
b_post_cond = ens ;
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
index 85d0655b52c..c9a28cfb2ae 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
@@ -99,6 +99,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_acsl/assigns_path.i:12: Warning:
Memory model hypotheses for function 'job':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(b + (..), &p); */
void job(int n, int *b);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index cb505e19fd9..e9965d8c184 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -1879,7 +1879,7 @@ Prove: true.
[wp] tests/wp_acsl/chunk_typing.i:21: Warning:
Memory model hypotheses for function 'function':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(i16 + (..), (char const *)x + (..));
requires \separated(i32 + (..), (char const *)x + (..));
requires \separated(i64 + (..), (char const *)x + (..));
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
index 91761e4ddc3..a6492896347 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
@@ -142,16 +142,16 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_acsl/funvar_inv.i:26: Warning:
Memory model hypotheses for function 'f':
- /*@ behavior hoare:
+ /*@ behavior wp_hoare:
ensures \separated(\result, (int *)G + (..)); */
int *f(void);
[wp] tests/wp_acsl/funvar_inv.i:40: Warning:
Memory model hypotheses for function 'f2':
- /*@ behavior hoare:
+ /*@ behavior wp_hoare:
ensures \separated(\result, (int *)G + (..)); */
int *f2(void);
[wp] tests/wp_acsl/funvar_inv.i:55: Warning:
Memory model hypotheses for function 'g':
- /*@ behavior hoare:
+ /*@ behavior wp_hoare:
ensures \separated(\result, (int *)G + (..)); */
int *g(void);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
index 193a70bc4bf..e261e262d43 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
@@ -236,11 +236,11 @@ Prove: false.
------------------------------------------------------------
[wp] tests/wp_acsl/pointer.i:63: Warning:
Memory model hypotheses for function 'compare':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(q + (..), &p); */
void compare(int *q);
[wp] tests/wp_acsl/pointer.i:73: Warning:
Memory model hypotheses for function 'absurd':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(q + (..), &p); */
void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
index d05bde7cc84..44a78cfe501 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
@@ -21,6 +21,6 @@
------------------------------------------------------------
[wp] tests/wp_acsl/assigns_path.i:12: Warning:
Memory model hypotheses for function 'job':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(b + (..), &p); */
void job(int n, int *b);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
index f5f8f9ccd56..7b0245a0e6e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
@@ -52,7 +52,7 @@
[wp] tests/wp_acsl/chunk_typing.i:21: Warning:
Memory model hypotheses for function 'function':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(i16 + (..), (char const *)x + (..));
requires \separated(i32 + (..), (char const *)x + (..));
requires \separated(i64 + (..), (char const *)x + (..));
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
index 5dee9e18dea..611e1df5b23 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
@@ -28,6 +28,6 @@
------------------------------------------------------------
[wp] tests/wp_acsl/pointer.i:73: Warning:
Memory model hypotheses for function 'absurd':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \separated(q + (..), &p); */
void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
index 60898d58685..bc584ec39a2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
@@ -28,6 +28,6 @@
------------------------------------------------------------
[wp] tests/wp_acsl/pointer.i:73: Warning:
Memory model hypotheses for function 'absurd':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(q + (..), &p); */
void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
index 65fbcabad5f..f5978426720 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
@@ -54,6 +54,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_bts/bts0843.i:13: Warning:
Memory model hypotheses for function 'f3':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(&p, &p->a); */
void f3(void);
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
index ebbd70f4cdb..beb9985d22d 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
@@ -67,6 +67,6 @@ Prove: global(L_two_24) != one_0.
------------------------------------------------------------
[wp] tests/wp_bts/bts_1828.i:56: Warning:
Memory model hypotheses for function 'global_frame':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(one, &zero); */
void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
index fdf25268ad2..1f183b1d30a 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
@@ -47,7 +47,7 @@ Prove: global(L_two_24) != one_0.
[wp] tests/wp_bts/bts_1828.i:56: Warning:
Memory model hypotheses for function 'global_frame':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(zero, one);
requires \valid(one);
requires \valid(zero);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
index a522bf115dd..c03a3a919ad 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
@@ -17,6 +17,6 @@
------------------------------------------------------------
[wp] tests/wp_bts/bts0843.i:13: Warning:
Memory model hypotheses for function 'f3':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(&p, &p->a); */
void f3(void);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
index 9bffe58d0b5..ae39dccf7da 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
@@ -19,6 +19,6 @@
------------------------------------------------------------
[wp] tests/wp_bts/bts_1828.i:56: Warning:
Memory model hypotheses for function 'global_frame':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(one, &zero); */
void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
index c85bac0087b..43305903b45 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
@@ -20,7 +20,7 @@
[wp] tests/wp_bts/bts_1828.i:56: Warning:
Memory model hypotheses for function 'global_frame':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(zero, one);
requires \valid(one);
requires \valid(zero);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
index d44fe2c4e6c..56bb306558b 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
@@ -55,7 +55,7 @@
[wp] tests/wp_gallery/frama_c_exo3_solved.old.c:73: Warning:
Memory model hypotheses for function 'equal_elements':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
index 68e0c5d7ad6..53078f53cb8 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
@@ -56,7 +56,7 @@
[wp] tests/wp_gallery/frama_c_exo3_solved.old.v2.c:56: Warning:
Memory model hypotheses for function 'equal_elements':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
index 70ff1ce19f1..3903ba3a3a3 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
@@ -47,7 +47,7 @@
[wp] tests/wp_gallery/frama_c_exo3_solved.old.c:73: Warning:
Memory model hypotheses for function 'equal_elements':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
index a87e532706d..1dfeafb91d5 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
@@ -48,7 +48,7 @@
[wp] tests/wp_gallery/frama_c_exo3_solved.old.v2.c:56: Warning:
Memory model hypotheses for function 'equal_elements':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle
index 793f91fafc8..8466ed1f89b 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle
@@ -196,24 +196,24 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:17: Warning:
Memory model hypotheses for function 'global_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(g_alias, (int *)global + (..), &g_alias);
*/
void global_alias(void);
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:24: Warning:
Memory model hypotheses for function 'global_no_alias':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(g_alias, &g_alias); */
void global_no_alias(void);
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:32: Warning:
Memory model hypotheses for function 'formal_alias':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(f_alias, (int *)global + (..)); */
void formal_alias(int *f_alias);
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:48: Warning:
Memory model hypotheses for function 'formal_alias_array':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &(*alias_array)[0 .. 1]);
requires \separated(alias_array + (..), (int *)global + (..));
*/
@@ -221,7 +221,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:61: Warning:
Memory model hypotheses for function 'field_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &x->x);
requires \separated(x, (int *)global + (..));
*/
@@ -229,7 +229,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:73: Warning:
Memory model hypotheses for function 'field_range_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &(x + (0 .. 3))->x);
requires \separated(x + (..), (int *)global + (..));
*/
@@ -237,7 +237,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:81: Warning:
Memory model hypotheses for function 'set_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
*/
@@ -245,7 +245,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:92: Warning:
Memory model hypotheses for function 'comprehension_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires
\separated(
(int *)global + (..), &g_alias,
@@ -256,7 +256,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:102: Warning:
Memory model hypotheses for function 'union_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
*/
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle
index 3da623e2493..d0a161603cf 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle
@@ -204,7 +204,7 @@ int *g_alias;
ensures \old(global[0]) ≡ global[0];
assigns *g_alias;
- behavior typed:
+ behavior wp_typed:
requires \separated(g_alias, (int *)global + (..), &g_alias);
*/
void global_alias(void)
@@ -217,7 +217,7 @@ void global_alias(void)
ensures *g_alias ≡ 1;
assigns *g_alias;
- behavior typed:
+ behavior wp_typed:
requires \separated(g_alias, &g_alias);
*/
void global_no_alias(void)
@@ -231,7 +231,7 @@ void global_no_alias(void)
ensures \old(global[0]) ≡ global[0];
assigns *f_alias;
- behavior typed:
+ behavior wp_typed:
requires \separated(f_alias, (int *)global + (..));
*/
void formal_alias(int *f_alias)
@@ -256,7 +256,7 @@ void formal_no_alias(int *f_alias)
ensures \old(global[0]) ≡ global[0];
assigns (*alias_array)[0 .. 1];
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &(*alias_array)[0 .. 1]);
requires \separated(alias_array + (..), (int *)global + (..));
*/
@@ -272,7 +272,7 @@ void formal_alias_array(int (*alias_array)[2])
ensures \old(global[0]) ≡ global[0];
assigns x->x;
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &x->x);
requires \separated(x, (int *)global + (..));
*/
@@ -287,7 +287,7 @@ void field_alias(struct X *x)
ensures \old(global[0]) ≡ global[0];
assigns (x + (0 .. 3))->x;
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &(x + (0 .. 3))->x);
requires \separated(x + (..), (int *)global + (..));
*/
@@ -302,7 +302,7 @@ void field_range_alias(struct X *x)
ensures \old(global[0]) ≡ global[0];
assigns {*g_alias, *f_alias};
- behavior typed:
+ behavior wp_typed:
requires
\separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
@@ -318,7 +318,7 @@ void set_alias(int *f_alias)
ensures \old(global[0]) ≡ global[0];
assigns {*alias | int *alias; alias ≡ \at(g_alias,Pre)};
- behavior typed:
+ behavior wp_typed:
requires
\separated(
(int *)global + (..), &g_alias,
@@ -336,7 +336,7 @@ void comprehension_alias(void)
ensures \old(global[0]) ≡ global[0];
assigns {*g_alias, *f_alias};
- behavior typed:
+ behavior wp_typed:
requires
\separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.res.oracle
index 1957a50c4e1..1bdd790f08e 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.res.oracle
@@ -70,22 +70,22 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_hoare/alias_escapes_hypotheses.i:8: Warning:
Memory model hypotheses for function 'f1':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
ensures \separated(\result, &a); */
int *f1(void);
[wp] tests/wp_hoare/alias_escapes_hypotheses.i:19: Warning:
Memory model hypotheses for function 'f3':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
ensures \separated(\result, &x); */
int *f3(int x);
[wp] tests/wp_hoare/alias_escapes_hypotheses.i:24: Warning:
Memory model hypotheses for function 'fp1':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p, &a);
ensures \separated(p, &a); */
void fp1(int **p);
[wp] tests/wp_hoare/alias_escapes_hypotheses.i:35: Warning:
Memory model hypotheses for function 'fp3':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
ensures \separated(p, &x); */
void fp3(int **p, int x);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
index 1fa158d4b18..242f5a77ff3 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
@@ -87,16 +87,16 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_hoare/byref.i:14: Warning:
Memory model hypotheses for function 'f':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(r); */
void f(int *r);
[wp] tests/wp_hoare/byref.i:20: Warning:
Memory model hypotheses for function 'wrong_without_ref':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int wrong_without_ref(int *q);
[wp] tests/wp_hoare/byref.i:31: Warning:
Memory model hypotheses for function 'pointer':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int pointer(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
index 3b0db526829..03056370c4a 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
@@ -498,23 +498,23 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_hoare/dispatch_var.i:12: Warning:
Memory model hypotheses for function 'ref_ctr':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(p); */
int ref_ctr(int *p);
[wp] tests/wp_hoare/dispatch_var.i:44: Warning:
Memory model hypotheses for function 'ref_bd':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int ref_bd(int *q);
[wp] tests/wp_hoare/dispatch_var.i:83: Warning:
Memory model hypotheses for function 'ref_valid':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(p1); */
int ref_valid(int *p1);
[wp] tests/wp_hoare/dispatch_var.i:133: Warning:
Memory model hypotheses for function 'ref_ctr_nr':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(ref, ref1, ref2);
requires \valid(ref);
requires \valid(ref1);
@@ -523,11 +523,11 @@ Prove: true.
int ref_ctr_nr(int *ref, int *ref1, int *ref2);
[wp] tests/wp_hoare/dispatch_var.i:158: Warning:
Memory model hypotheses for function 'ref_ctr_nstars':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(pp); */
int ref_ctr_nstars(int **pp);
[wp] tests/wp_hoare/dispatch_var.i:194: Warning:
Memory model hypotheses for function 'g':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(pg); */
int g(int *pg);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
index 9920ee4d4ce..f4ddcc68450 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
@@ -487,21 +487,21 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_hoare/dispatch_var2.i:16: Warning:
Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(rp); */
void reset(int *rp);
[wp] tests/wp_hoare/dispatch_var2.i:23: Warning:
Memory model hypotheses for function 'incr':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(ip); */
void incr(int *ip);
[wp] tests/wp_hoare/dispatch_var2.i:31: Warning:
Memory model hypotheses for function 'load':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(lp); */
int load(int *lp);
[wp] tests/wp_hoare/dispatch_var2.i:70: Warning:
Memory model hypotheses for function 'call_param_ref':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
index 932c183de67..1e932094cc2 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
@@ -212,21 +212,21 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_hoare/dispatch_var2.i:16: Warning:
Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(rp); */
void reset(int *rp);
[wp] tests/wp_hoare/dispatch_var2.i:23: Warning:
Memory model hypotheses for function 'incr':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(ip); */
void incr(int *ip);
[wp] tests/wp_hoare/dispatch_var2.i:31: Warning:
Memory model hypotheses for function 'load':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(lp); */
int load(int *lp);
[wp] tests/wp_hoare/dispatch_var2.i:70: Warning:
Memory model hypotheses for function 'call_param_ref':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
index c7395b1a724..bf4453996e1 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
@@ -143,13 +143,13 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_hoare/reference.i:14: Warning:
Memory model hypotheses for function 'f':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(p); */
int f(int *p);
[wp] tests/wp_hoare/reference.i:30: Warning:
Memory model hypotheses for function 'f2':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(p2, q);
requires \valid(p2);
requires \valid(q);
@@ -157,16 +157,16 @@ Prove: true.
int f2(int *p2, int *q);
[wp] tests/wp_hoare/reference.i:37: Warning:
Memory model hypotheses for function 'call_f2':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(ptr); */
int call_f2(int *ptr, int y);
[wp] tests/wp_hoare/reference.i:48: Warning:
Memory model hypotheses for function 'call_global':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(gl); */
int call_global(void);
[wp] tests/wp_hoare/reference.i:60: Warning:
Memory model hypotheses for function 'write':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(pa); */
void write(int kb, int *pa);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index f816e6df044..49db1a0e743 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -253,20 +253,20 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_hoare/reference_and_struct.i:15: Warning:
Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(p); */
void reset(struct T *p);
[wp] tests/wp_hoare/reference_and_struct.i:48: Warning:
Memory model hypotheses for function 'call_reset_5_tps':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated((struct T **)tps + (..), tps[9] + (0 .. 4));
*/
void call_reset_5_tps(void);
[wp] tests/wp_hoare/reference_and_struct.i:88: Warning:
Memory model hypotheses for function 'load_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(hp + (..), (int *)reg_load + (..));
*/
void load_5(int *hp);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
index fe649246798..e9a8a909640 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
@@ -404,14 +404,14 @@ Prove: true.
[wp] tests/wp_hoare/reference_array.i:24: Warning:
Memory model hypotheses for function 'load_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(hp + (..), (int *)reg_load + (..));
*/
void load_5(int *hp);
[wp] tests/wp_hoare/reference_array.i:31: Warning:
Memory model hypotheses for function 'add_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires
\separated(gp + (..), (int *)reg_load + (..), (int *)reg_add + (..));
*/
@@ -419,14 +419,14 @@ Prove: true.
[wp] tests/wp_hoare/reference_array.i:45: Warning:
Memory model hypotheses for function 'load_1_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(lp + (..), (int *)reg_load + (..));
*/
void load_1_5(int (*lp)[5]);
[wp] tests/wp_hoare/reference_array.i:52: Warning:
Memory model hypotheses for function 'add_1_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires
\separated(ap + (..), (int *)reg_load + (..), (int *)reg_add + (..));
*/
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
index dfd54b08846..576a7de621c 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
@@ -39,6 +39,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_hoare/reference_array_simple.i:40: Warning:
Memory model hypotheses for function 'call_f3':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
ensures \separated(\result, (int **)tp + (..)); */
int *call_f3(void);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
index bb63bebf59a..b99e1013102 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
@@ -71,7 +71,7 @@ Prove: d != c.
[wp] tests/wp_hoare/refguards.i:10: Warning:
Memory model hypotheses for function 'f':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(c, d, {a + (..), b + (..)});
requires \valid(c);
requires \valid(d);
@@ -80,7 +80,7 @@ Prove: d != c.
[wp] tests/wp_hoare/refguards.i:25: Warning:
Memory model hypotheses for function 'h':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(c, d);
requires \valid(c);
requires \valid(d);
@@ -89,7 +89,7 @@ Prove: d != c.
[wp] tests/wp_hoare/refguards.i:39: Warning:
Memory model hypotheses for function 's':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(c, d);
requires \valid(c);
requires \valid(d);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
index 99cd98673ce..ca6a95729cf 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
@@ -51,24 +51,24 @@
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:17: Warning:
Memory model hypotheses for function 'global_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(g_alias, (int *)global + (..), &g_alias);
*/
void global_alias(void);
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:24: Warning:
Memory model hypotheses for function 'global_no_alias':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(g_alias, &g_alias); */
void global_no_alias(void);
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:32: Warning:
Memory model hypotheses for function 'formal_alias':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(f_alias, (int *)global + (..)); */
void formal_alias(int *f_alias);
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:48: Warning:
Memory model hypotheses for function 'formal_alias_array':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &(*alias_array)[0 .. 1]);
requires \separated(alias_array + (..), (int *)global + (..));
*/
@@ -76,7 +76,7 @@
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:61: Warning:
Memory model hypotheses for function 'field_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &x->x);
requires \separated(x, (int *)global + (..));
*/
@@ -84,7 +84,7 @@
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:73: Warning:
Memory model hypotheses for function 'field_range_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &(x + (0 .. 3))->x);
requires \separated(x + (..), (int *)global + (..));
*/
@@ -92,7 +92,7 @@
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:81: Warning:
Memory model hypotheses for function 'set_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
*/
@@ -100,7 +100,7 @@
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:92: Warning:
Memory model hypotheses for function 'comprehension_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires
\separated(
(int *)global + (..), &g_alias,
@@ -111,7 +111,7 @@
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:102: Warning:
Memory model hypotheses for function 'union_alias':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
*/
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
index 816e897df18..8d3ab297b01 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
@@ -28,16 +28,16 @@
------------------------------------------------------------
[wp] tests/wp_hoare/byref.i:14: Warning:
Memory model hypotheses for function 'f':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(r); */
void f(int *r);
[wp] tests/wp_hoare/byref.i:20: Warning:
Memory model hypotheses for function 'wrong_without_ref':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int wrong_without_ref(int *q);
[wp] tests/wp_hoare/byref.i:31: Warning:
Memory model hypotheses for function 'pointer':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int pointer(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
index aa66d23b2fc..ab588be9a5c 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
@@ -101,23 +101,23 @@
------------------------------------------------------------
[wp] tests/wp_hoare/dispatch_var.i:12: Warning:
Memory model hypotheses for function 'ref_ctr':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(p); */
int ref_ctr(int *p);
[wp] tests/wp_hoare/dispatch_var.i:44: Warning:
Memory model hypotheses for function 'ref_bd':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int ref_bd(int *q);
[wp] tests/wp_hoare/dispatch_var.i:83: Warning:
Memory model hypotheses for function 'ref_valid':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(p1); */
int ref_valid(int *p1);
[wp] tests/wp_hoare/dispatch_var.i:133: Warning:
Memory model hypotheses for function 'ref_ctr_nr':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(ref, ref1, ref2);
requires \valid(ref);
requires \valid(ref1);
@@ -126,11 +126,11 @@
int ref_ctr_nr(int *ref, int *ref1, int *ref2);
[wp] tests/wp_hoare/dispatch_var.i:158: Warning:
Memory model hypotheses for function 'ref_ctr_nstars':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(pp); */
int ref_ctr_nstars(int **pp);
[wp] tests/wp_hoare/dispatch_var.i:194: Warning:
Memory model hypotheses for function 'g':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(pg); */
int g(int *pg);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
index 9172fe5d07b..701b7f065df 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
@@ -51,21 +51,21 @@
------------------------------------------------------------
[wp] tests/wp_hoare/dispatch_var2.i:16: Warning:
Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(rp); */
void reset(int *rp);
[wp] tests/wp_hoare/dispatch_var2.i:23: Warning:
Memory model hypotheses for function 'incr':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(ip); */
void incr(int *ip);
[wp] tests/wp_hoare/dispatch_var2.i:31: Warning:
Memory model hypotheses for function 'load':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(lp); */
int load(int *lp);
[wp] tests/wp_hoare/dispatch_var2.i:70: Warning:
Memory model hypotheses for function 'call_param_ref':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
index 26521bbd90e..699d53b4162 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
@@ -51,21 +51,21 @@
------------------------------------------------------------
[wp] tests/wp_hoare/dispatch_var2.i:16: Warning:
Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(rp); */
void reset(int *rp);
[wp] tests/wp_hoare/dispatch_var2.i:23: Warning:
Memory model hypotheses for function 'incr':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(ip); */
void incr(int *ip);
[wp] tests/wp_hoare/dispatch_var2.i:31: Warning:
Memory model hypotheses for function 'load':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(lp); */
int load(int *lp);
[wp] tests/wp_hoare/dispatch_var2.i:70: Warning:
Memory model hypotheses for function 'call_param_ref':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(q); */
int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
index f90e23c73a5..6fa2c547d93 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
@@ -38,13 +38,13 @@
------------------------------------------------------------
[wp] tests/wp_hoare/reference.i:14: Warning:
Memory model hypotheses for function 'f':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(p); */
int f(int *p);
[wp] tests/wp_hoare/reference.i:30: Warning:
Memory model hypotheses for function 'f2':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(p2, q);
requires \valid(p2);
requires \valid(q);
@@ -52,16 +52,16 @@
int f2(int *p2, int *q);
[wp] tests/wp_hoare/reference.i:37: Warning:
Memory model hypotheses for function 'call_f2':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(ptr); */
int call_f2(int *ptr, int y);
[wp] tests/wp_hoare/reference.i:48: Warning:
Memory model hypotheses for function 'call_global':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(gl); */
int call_global(void);
[wp] tests/wp_hoare/reference.i:60: Warning:
Memory model hypotheses for function 'write':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(pa); */
void write(int kb, int *pa);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
index 48133b9d6ee..a4e3ed789ba 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
@@ -51,20 +51,20 @@
------------------------------------------------------------
[wp] tests/wp_hoare/reference_and_struct.i:15: Warning:
Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(p); */
void reset(struct T *p);
[wp] tests/wp_hoare/reference_and_struct.i:48: Warning:
Memory model hypotheses for function 'call_reset_5_tps':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated((struct T **)tps + (..), tps[9] + (0 .. 4));
*/
void call_reset_5_tps(void);
[wp] tests/wp_hoare/reference_and_struct.i:88: Warning:
Memory model hypotheses for function 'load_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(hp + (..), (int *)reg_load + (..));
*/
void load_5(int *hp);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
index 4a84b4eb4b8..2df672162a7 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
@@ -54,14 +54,14 @@
[wp] tests/wp_hoare/reference_array.i:24: Warning:
Memory model hypotheses for function 'load_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(hp + (..), (int *)reg_load + (..));
*/
void load_5(int *hp);
[wp] tests/wp_hoare/reference_array.i:31: Warning:
Memory model hypotheses for function 'add_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires
\separated(gp + (..), (int *)reg_load + (..), (int *)reg_add + (..));
*/
@@ -69,14 +69,14 @@
[wp] tests/wp_hoare/reference_array.i:45: Warning:
Memory model hypotheses for function 'load_1_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(lp + (..), (int *)reg_load + (..));
*/
void load_1_5(int (*lp)[5]);
[wp] tests/wp_hoare/reference_array.i:52: Warning:
Memory model hypotheses for function 'add_1_5':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires
\separated(ap + (..), (int *)reg_load + (..), (int *)reg_add + (..));
*/
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
index fb6e0358382..7b00985377b 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
@@ -16,6 +16,6 @@
------------------------------------------------------------
[wp] tests/wp_hoare/reference_array_simple.i:40: Warning:
Memory model hypotheses for function 'call_f3':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
ensures \separated(\result, (int **)tp + (..)); */
int *call_f3(void);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
index 9a42e648075..3fba6a750b4 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
@@ -25,7 +25,7 @@
[wp] tests/wp_hoare/refguards.i:10: Warning:
Memory model hypotheses for function 'f':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(c, d, {a + (..), b + (..)});
requires \valid(c);
requires \valid(d);
@@ -34,7 +34,7 @@
[wp] tests/wp_hoare/refguards.i:25: Warning:
Memory model hypotheses for function 'h':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(c, d);
requires \valid(c);
requires \valid(d);
@@ -43,7 +43,7 @@
[wp] tests/wp_hoare/refguards.i:39: Warning:
Memory model hypotheses for function 's':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(c, d);
requires \valid(c);
requires \valid(d);
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 91365d446b7..ad37a67830b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -374,21 +374,21 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_plugin/dynamic.i:41: Warning:
Memory model hypotheses for function 'guarded_call':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p, &X); */
void guarded_call(struct S *p);
[wp] tests/wp_plugin/dynamic.i:63: Warning:
Memory model hypotheses for function 'behavior':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p + (..), &X1); */
int behavior(int (*p)(void));
[wp] tests/wp_plugin/dynamic.i:76: Warning:
Memory model hypotheses for function 'some_behaviors':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p + (..), &X1); */
int some_behaviors(int (*p)(void));
[wp] tests/wp_plugin/dynamic.i:85: Warning:
Memory model hypotheses for function 'missing_context':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p, &X1); */
int missing_context(int (*p)(void));
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
index 6f296e1d079..07bb9ac0b9f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
@@ -102,11 +102,11 @@ Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), -5), 10).
------------------------------------------------------------
[wp] tests/wp_plugin/overassign.i:14: Warning:
Memory model hypotheses for function 'f1_ok':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p + (0 .. 9), &p); */
void f1_ok(void);
[wp] tests/wp_plugin/overassign.i:17: Warning:
Memory model hypotheses for function 'f2_ok':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p + (10 .. 19), &p); */
void f2_ok(void);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
index d557391b191..19f37ddeabb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
@@ -35,7 +35,7 @@ Prove: true.
[wp] tests/wp_plugin/post_assigns.i:12: Warning:
Memory model hypotheses for function 'receive':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(message + (..), &size);
ensures \separated(message + (0 .. \at(size,Post)), &size);
*/
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
index 61c35549a7f..e5d8aa84c06 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
@@ -68,20 +68,22 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_plugin/sep.i:18: Warning:
Memory model hypotheses for function 'f2_p_a':
- /*@ behavior typed_caveat:
+ /*@ behavior wp_typed_caveat:
requires \separated(p, &a);
requires \valid(p); */
void f2_p_a(int *p);
[wp] tests/wp_plugin/sep.i:22: Warning:
Memory model hypotheses for function 'f3_p_ab':
- /*@ behavior typed_caveat:
- requires \separated(p, &a, &b);
- requires \valid(p); */
+ /*@
+ behavior wp_typed_caveat:
+ requires \separated(p, &a, &b);
+ requires \valid(p);
+ */
void f3_p_ab(int *p);
[wp] tests/wp_plugin/sep.i:26: Warning:
Memory model hypotheses for function 'f4_pq_ab':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(p, q, &a, &b);
requires \valid(p);
requires \valid(q);
@@ -90,7 +92,7 @@ Prove: true.
[wp] tests/wp_plugin/sep.i:30: Warning:
Memory model hypotheses for function 'f5_pq':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(p, q);
requires \valid(p);
requires \valid(q);
@@ -99,7 +101,7 @@ Prove: true.
[wp] tests/wp_plugin/sep.i:34: Warning:
Memory model hypotheses for function 'f6_Pa':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(p + (..), &a);
requires \valid(p + (..));
*/
@@ -107,7 +109,7 @@ Prove: true.
[wp] tests/wp_plugin/sep.i:43: Warning:
Memory model hypotheses for function 'f7_pq_ad':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(p, q, &a, &d);
requires \valid(p);
requires \valid(q);
@@ -116,7 +118,7 @@ Prove: true.
[wp] tests/wp_plugin/sep.i:49: Warning:
Memory model hypotheses for function 'f8_pq_a':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(p, q, &a);
requires \valid(p);
requires \valid(q);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
index dbd14586d29..00afcb0afdf 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
@@ -45,7 +45,7 @@ Prove: valid_rw(Malloc_0, p, 2).
[wp] tests/wp_plugin/subset_fopen.c:13: Warning:
Memory model hypotheses for function 'fopen':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(&_p__fc_fopen, {filename + (..), mode + (..)});
ensures \separated(\result, &_p__fc_fopen);
*/
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
index 015937705a8..2df04eb693e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
@@ -37,6 +37,6 @@ Prove: EqS1_st_v(w, w_1).
------------------------------------------------------------
[wp] tests/wp_plugin/volatile.i:32: Warning:
Memory model hypotheses for function 'job_struct_assigns':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p, &sv); */
void job_struct_assigns(struct st_v *p);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
index 8736e619bd1..63e2b65a2c4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
@@ -71,6 +71,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_plugin/volatile.i:32: Warning:
Memory model hypotheses for function 'job_struct_assigns':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p, &sv); */
void job_struct_assigns(struct st_v *p);
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 f2e983f6020..e3e408c44c1 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
@@ -69,21 +69,21 @@
------------------------------------------------------------
[wp] tests/wp_plugin/dynamic.i:41: Warning:
Memory model hypotheses for function 'guarded_call':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p, &X); */
void guarded_call(struct S *p);
[wp] tests/wp_plugin/dynamic.i:63: Warning:
Memory model hypotheses for function 'behavior':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p + (..), &X1); */
int behavior(int (*p)(void));
[wp] tests/wp_plugin/dynamic.i:76: Warning:
Memory model hypotheses for function 'some_behaviors':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p + (..), &X1); */
int some_behaviors(int (*p)(void));
[wp] tests/wp_plugin/dynamic.i:85: Warning:
Memory model hypotheses for function 'missing_context':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p, &X1); */
int missing_context(int (*p)(void));
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
index 48f494c79a7..76de1d842d7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
@@ -29,11 +29,11 @@
------------------------------------------------------------
[wp] tests/wp_plugin/overassign.i:14: Warning:
Memory model hypotheses for function 'f1_ok':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p + (0 .. 9), &p); */
void f1_ok(void);
[wp] tests/wp_plugin/overassign.i:17: Warning:
Memory model hypotheses for function 'f2_ok':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(p + (10 .. 19), &p); */
void f2_ok(void);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
index bde4fe1a240..7aee3baaefa 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
@@ -17,7 +17,7 @@
[wp] tests/wp_plugin/post_assigns.i:12: Warning:
Memory model hypotheses for function 'receive':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(message + (..), &size);
ensures \separated(message + (0 .. \at(size,Post)), &size);
*/
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
index 4fe11f354b8..55f410c2efe 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
@@ -18,7 +18,7 @@
[wp] tests/wp_plugin/subset_fopen.c:13: Warning:
Memory model hypotheses for function 'fopen':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(&_p__fc_fopen, {filename + (..), mode + (..)});
ensures \separated(\result, &_p__fc_fopen);
*/
diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
index bc47567d84e..598ec02c22b 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
@@ -28,7 +28,7 @@ Prove: `x_2 = `x_1.
[wp] tests/wp_tip/chunk_printing.i:19: Warning:
Memory model hypotheses for function 'get_int':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(v, &y);
ensures \separated(\result, &y);
*/
@@ -36,7 +36,7 @@ Prove: `x_2 = `x_1.
[wp] tests/wp_tip/chunk_printing.i:25: Warning:
Memory model hypotheses for function 'get_uint':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(v, &y);
ensures \separated(\result, &y);
*/
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
index 21e31a09591..b7a091489fb 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
@@ -21,7 +21,7 @@ Prove: P_equal(1, 1).
[wp] tests/wp_typed/mvar.i:8: Warning:
Memory model hypotheses for function 'Write':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(p + (..), (char *)A + (..));
requires \separated(p + (0 ..), (char *)A + (..));
*/
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
index 2c2ed44ef41..a58a157b823 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
@@ -21,7 +21,7 @@ Prove: P_equal(1, 1).
[wp] tests/wp_typed/mvar.i:8: Warning:
Memory model hypotheses for function 'Write':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(p + (..), (char *)A + (..));
requires \separated(p + (0 ..), (char *)A + (..));
*/
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
index c0c24ca13d8..8da6181fa48 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
@@ -61,6 +61,6 @@ Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
------------------------------------------------------------
[wp] tests/wp_typed/unit_alloc.i:34: Warning:
Memory model hypotheses for function 'h':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
ensures \separated(\result, &x); */
int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
index ff04631dd24..1444f81cf6e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
@@ -61,6 +61,6 @@ Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
------------------------------------------------------------
[wp] tests/wp_typed/unit_alloc.i:34: Warning:
Memory model hypotheses for function 'h':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
ensures \separated(\result, &x); */
int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
index 1619506b6e9..2ffd064c6d5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
@@ -12,6 +12,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_typed/unit_ite.i:3: Warning:
Memory model hypotheses for function 'check':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(p); */
void check(int x, int *p);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
index 55340b288d2..7a7b1b25d56 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
@@ -29,7 +29,7 @@ Prove: true.
[wp] tests/wp_typed/unit_labels.i:7: Warning:
Memory model hypotheses for function 'duplet':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(pi, pj, a + (..));
requires \valid(pi);
requires \valid(pj);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
index 0417f4d5c31..c64b78b42d0 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
@@ -19,6 +19,6 @@ Prove: false.
------------------------------------------------------------
[wp] tests/wp_typed/unit_loopscope.i:9: Warning:
Memory model hypotheses for function 'f':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(written); */
void f(unsigned int *written);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
index fe5762e157d..a1ac6afa9ad 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
@@ -118,7 +118,7 @@ Prove: true.
[wp] tests/wp_typed/user_injector.i:58: Warning:
Memory model hypotheses for function 'job':
/*@
- behavior typed:
+ behavior wp_typed:
requires
\separated(
error, (int *)service_id + (..), (int *)service_result + (..), &seq,
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
index b46f36ca8ac..e571b4fc2cc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
@@ -43,7 +43,7 @@ Prove: true.
[wp] tests/wp_typed/user_swap.i:13: Warning:
Memory model hypotheses for function 'swap':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(a, b);
requires \valid(a);
requires \valid(b);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
index a80625768fa..78b8c7b8aa1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
@@ -16,7 +16,7 @@
[wp] tests/wp_typed/mvar.i:8: Warning:
Memory model hypotheses for function 'Write':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(p + (..), (char *)A + (..));
requires \separated(p + (0 ..), (char *)A + (..));
*/
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
index b1b2521268f..712b3446883 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
@@ -22,6 +22,6 @@
------------------------------------------------------------
[wp] tests/wp_typed/unit_alloc.i:34: Warning:
Memory model hypotheses for function 'h':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
ensures \separated(\result, &x); */
int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
index 8ce55b8c1ef..d0b9a9657e2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
@@ -22,6 +22,6 @@
------------------------------------------------------------
[wp] tests/wp_typed/unit_alloc.i:34: Warning:
Memory model hypotheses for function 'h':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
ensures \separated(\result, &x); */
int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
index 6a7a2b81e80..a5bd933b1bc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
@@ -16,6 +16,6 @@
------------------------------------------------------------
[wp] tests/wp_typed/unit_loopscope.i:9: Warning:
Memory model hypotheses for function 'f':
- /*@ behavior typed_ref:
+ /*@ behavior wp_typed_ref:
requires \valid(written); */
void f(unsigned int *written);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
index 3cb90f7aac4..68842329caa 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
@@ -32,7 +32,7 @@
[wp] tests/wp_typed/user_injector.i:58: Warning:
Memory model hypotheses for function 'job':
/*@
- behavior typed:
+ behavior wp_typed:
requires
\separated(
error, (int *)service_id + (..), (int *)service_result + (..), &seq,
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
index aff929f01af..ad44942e79c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
@@ -28,7 +28,7 @@
[wp] tests/wp_typed/user_injector.i:58: Warning:
Memory model hypotheses for function 'job':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires
\separated(
error, (int *)service_id + (..), (int *)service_result + (..), &seq,
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
index 299ef52752e..d37ff58f250 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
@@ -19,7 +19,7 @@
[wp] tests/wp_typed/user_swap.i:13: Warning:
Memory model hypotheses for function 'swap':
/*@
- behavior typed_ref:
+ behavior wp_typed_ref:
requires \separated(a, b);
requires \valid(a);
requires \valid(b);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
index ebe14ffdae0..7f6f4e13162 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
@@ -71,7 +71,7 @@ Prove: P_OBS(x_2, x_3, x_4).
[wp] tests/wp_usage/caveat.i:17: Warning:
Memory model hypotheses for function 'implicit':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(a, r);
requires \valid(a);
requires \valid(r);
@@ -80,7 +80,7 @@ Prove: P_OBS(x_2, x_3, x_4).
[wp] tests/wp_usage/caveat.i:32: Warning:
Memory model hypotheses for function 'explicit':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(a, r);
requires \valid(a);
requires \valid(r);
@@ -89,7 +89,7 @@ Prove: P_OBS(x_2, x_3, x_4).
[wp] tests/wp_usage/caveat.i:47: Warning:
Memory model hypotheses for function 'observer':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(a, r);
requires \valid(a);
requires \valid(r);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
index 736fa74fbf8..bd126749ac2 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -100,7 +100,7 @@ Prove: true.
[wp] tests/wp_usage/caveat2.i:17: Warning:
Memory model hypotheses for function 'job':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(p, b + (..));
requires \valid(b + (..));
requires \valid(p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
index b0856e556ee..82cb1e098dc 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
@@ -156,6 +156,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_usage/caveat_range.i:16: Warning:
Memory model hypotheses for function 'reset':
- /*@ behavior typed_caveat:
+ /*@ behavior wp_typed_caveat:
requires \valid(p + (..)); */
void reset(struct S *p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
index 76498068b73..1f25e6893d0 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
@@ -21,6 +21,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_usage/global.c:16: Warning:
Memory model hypotheses for function 'foo':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(a, &GLOBAL); */
void foo(int *a);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
index 221fdfb3bc9..3489aa28745 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
@@ -21,7 +21,9 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_usage/global.c:16: Warning:
Memory model hypotheses for function 'foo':
- /*@ behavior typed_ref:
- requires \separated(a, &GLOBAL);
- requires \valid(a); */
+ /*@
+ behavior wp_typed_ref:
+ requires \separated(a, &GLOBAL);
+ requires \valid(a);
+ */
void foo(int *a);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
index 7d5d683720a..c15cbee10c3 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
@@ -170,7 +170,7 @@ Prove: true.
[wp] tests/wp_usage/issue-189-bis.i:48: Warning:
Memory model hypotheses for function 'memcpy_context_vars':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(src, dst);
requires \valid(dst);
requires \valid(src);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
index cfc85d0a9b7..5cd9f57c585 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
@@ -25,7 +25,7 @@ Prove: true.
[wp] tests/wp_usage/issue-189.i:16: Warning:
Memory model hypotheses for function 'f':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(ptr, src);
requires \valid(ptr);
*/
diff --git a/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
index e0ce794b3c5..7d8d28eb790 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
@@ -19,6 +19,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_usage/ref-usage-lemmas.i:26: Warning:
Memory model hypotheses for function 'foo':
- /*@ behavior typed:
+ /*@ behavior wp_typed:
requires \separated(x, &b); */
void foo(int *x);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
index dca6dab77af..86f77567c02 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
@@ -23,7 +23,7 @@
[wp] tests/wp_usage/caveat2.i:17: Warning:
Memory model hypotheses for function 'job':
/*@
- behavior typed_caveat:
+ behavior wp_typed_caveat:
requires \separated(p, b + (..));
requires \valid(b + (..));
requires \valid(p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
index c931af606d2..9a6fb8012b0 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
@@ -24,6 +24,6 @@
------------------------------------------------------------
[wp] tests/wp_usage/caveat_range.i:16: Warning:
Memory model hypotheses for function 'reset':
- /*@ behavior typed_caveat:
+ /*@ behavior wp_typed_caveat:
requires \valid(p + (..)); */
void reset(struct S *p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
index d0d733d8c65..e73a38c074f 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
@@ -23,7 +23,7 @@
[wp] tests/wp_usage/issue-189-bis.i:48: Warning:
Memory model hypotheses for function 'memcpy_context_vars':
/*@
- behavior typed:
+ behavior wp_typed:
requires \separated(src, dst);
requires \valid(dst);
requires \valid(src);
--
GitLab