diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 5ad6dcba1541f74ac8d611f94c1851349345542d..b142d6f84c57c28632928cd7bd13da1362defadb 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 85d0655b52c9c6f00e321eba103e7d31330535af..c9a28cfb2ae210a0e5e3161fef820e7c1f8ff088 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 cb505e19fd91db51fd8c8581d8930518c446386f..e9965d8c184b6a34ceb012ba529c0bce3040c5ca 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 91761e4ddc32ac42971be6cc9cfe19ebe60996dd..a6492896347e183c19f0db5379accd1e4c56183e 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 193a70bc4bfe20e9e1f0a2ff6b6a970071934ab1..e261e262d4301be01fe9cddb106761c86a568653 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 d05bde7cc8411f65f2c876e5fc58b7a4d0909523..44a78cfe5015b349177603e2c6ae694393fea054 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 f5f8f9ccd569d3afe1f92d928c09cb6f971f37c9..7b0245a0e6efb58b2d203320f97dd91e6ecff2c3 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 5dee9e18dea7a397b0b68dd1166c5017a69e42f6..611e1df5b2346833d7a864082944152d1fc2d6fe 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 60898d58685b7b6774435259868746d719fa009a..bc584ec39a2bd1f1c490cfcf15d0c7c3e933b0e6 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 65fbcabad5f6feb716502491e09692950ecd13ca..f5978426720ef2f96d406680c2c8728e7d414f59 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 ebbd70f4cdb5c0ab25cbdbe4851fd25508a7ad74..beb9985d22d92f771e20d79592ca3ab408a2442e 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 fdf25268ad263c656d0595867530283b170c00b0..1f183b1d30a1530c5c404f9a38f7ed12fec5d9ff 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 a522bf115dd4084100bbd4a728c2407f844dd3ca..c03a3a919adbf377b4708ec6c4893de1c1af9bcd 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 9bffe58d0b5888097457e33f13a614c0923d1380..ae39dccf7daf8069747276e8f126cee91ea56590 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 c85bac0087bbe0e5464f4eb837e7ffb174497af5..43305903b452ccabf5e96e46b022d2bfe3c1ffce 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 d44fe2c4e6cf3b831856e5f9a29033424f325831..56bb306558b56d74141556fc1b026d735ef9cfe9 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 68e0c5d7ad61be97d82deb34c0685928eccfe3ab..53078f53cb88bbc0681c1ce463aef6b08bf1de0e 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 70ff1ce19f1e4c50cb97c8ec8ae310d3df64c9ba..3903ba3a3a32a691f6e6e2bce73a83b71362f378 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 a87e532706dc3c93fcf82afc8e891eb1e836b190..1dfeafb91d559189ced438c76169d59f9f36c303 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 793f91fafc8b11ae56f885196d13c202f7031b25..8466ed1f89b2a33727f083057237518820c3eabb 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 3da623e24931019ca8f1a8fbdc64132f1611c015..d0a161603cf991c1248998ebc3fc7474a1dbfb09 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 1957a50c4e1d970781f3c142a07be38a9eaf8828..1bdd790f08ef4b1b4539ed7f810ed986367b36f8 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 1fa158d4b18a42536b46fc8d617c79c8addd69dc..242f5a77ff302f76bdf9ebf17e7311f394fdfb07 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 3b0db52682911a8d6ab8cc90fdf69221793feba4..03056370c4a6760b6e4e1e2f3662a4c7bf5753a0 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 9920ee4d4ce39ff13cde465cd8e8a4e73071e3e1..f4ddcc684505866177434a0690f31e787b73a9da 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 932c183de67c2c15fac39260964ad91f34d3e149..1e932094cc2e77a3a6e96c4fbe00a3594a0f4ca6 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 c7395b1a724d5c497e330ed30c33d8df230504aa..bf4453996e1f0c3f7c0390b232a6c5e86e4608d0 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 f816e6df044db643780fcfefb4a18db78d8d6ee4..49db1a0e74357cad28001df60cbecbc64387bd56 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 fe649246798c8210ee07cd60014b3b8020249e24..e9a8a909640530b5909b8fe20599229d74472b18 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 dfd54b08846ad1d56c15fbb2b2bd952d1342f4d0..576a7de621ccb62b85b0a62392d20f0042b7c374 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 bb63bebf59aac3371d4afd549278466915ae84f5..b99e101310280266d0fc3cf756af8bf32fabd5d8 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 99cd98673ce8c30cb84f9b4592bd0be80b8c2d4b..ca6a95729cf10ea40560483fdf25db1e55cf903c 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 816e897df18e973f7469fde30c0b26c8d9cc67ef..8d3ab297b0161e20ed2a81b25a6f776b2f30112d 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 aa66d23b2fc824f2a9fcc290903ad10e2472f60b..ab588be9a5c14dfaecd979bc01834341e6c05cef 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 9172fe5d07b12a7013a117e077c9c88d97db1c53..701b7f065df03139920f6017569bbcc18b9be799 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 26521bbd90e8db80954e4a8e6971f3297d08abc0..699d53b416274a7ffe806af5c041dfef6293f5a0 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 f90e23c73a56d68a5670142e2331b020f91fdff6..6fa2c547d939685057c4e3ce840a76ab810eb7e8 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 48133b9d6ee5bb8492567fd1e13d61fd9825ecab..a4e3ed789ba72a4140a2684e13f6d9013acdb46b 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 4a84b4eb4b8c8afb7e12d1857d5493d093e7bd80..2df672162a74515bca9c937e13606ac49af6b508 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 fb6e0358382668a5afa565e2f2b29453d01b4758..7b00985377bce93debde6c76f033a655f68b5e06 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 9a42e6480755beabc8ff4e171354431611c8e39a..3fba6a750b4f8d97faebe8f14aca0aa61237fea0 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 91365d446b74714bc8e525b1a263f63b68ea802e..ad37a67830bf85dd03dd6f3a058108f367ee9ea3 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 6f296e1d079de70a596bdd4040d8e4c6ece6ec89..07bb9ac0b9f9b3ef4f2352b015497127b6465484 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 d557391b19112f81757a1ec381d4c8654843220f..19f37ddeabbbc865df8040fd01e2f84dde96bd3c 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 61c35549a7f26dec27865a64f21521a7eb2621fe..e5d8aa84c061c2c39a06fe1f5257ffadeaea8003 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 dbd14586d294b694662a1f3307a020de0b031944..00afcb0afdf228e6888c4e919210cda1e0acfc7a 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 015937705a8d43b4ee893e04224eaaee149f5f51..2df04eb693e0221ae001c0fbd615d432dec4cd3c 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 8736e619bd18aeb73a6fd945870497310334e0a9..63e2b65a2c49a5ca6bf4edcaf5f179a9121e0b6d 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 f2e983f6020cd64b9e459140833506dde59690e1..e3e408c44c11240b3f222cc20901d0fcf6b2d977 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 48f494c79a7826f0372c9abb423449505d239ab4..76de1d842d7dfc708fbbd538f479ca9b714345e9 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 bde4fe1a2403a2c73bdcb61ae4a868fb1c46b58d..7aee3baaefaec1b15258306f2a55889dd80911ba 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 4fe11f354b827f32749dbd36c53e56e84aa47a45..55f410c2efe359058200eed08eb2f0595a0ab2fc 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 bc47567d84ec4e98ad6468258246726a564d6c73..598ec02c22b31480783d0e71c8ee206b3c3ca225 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 21e31a09591178e574a7787a5a2870513301fd03..b7a091489fb93752d1a9cc9aca36bad12fb18539 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 2c2ed44ef412f4455658321defa7791f181de35e..a58a157b823fe1a0b4e6ad4fa3dadced366513f7 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 c0c24ca13d883c91904d2ddd9f7a9da420afcf19..8da6181fa48f73c8f2e46181035f04cd3962ddbe 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 ff04631dd24c76acef4536e3778263e304db9300..1444f81cf6e1e9bac9d8b672b5e5dd31bbb95c26 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 1619506b6e983f527754d34c19c907d7547733a8..2ffd064c6d514e4f7cb6597ab668144d4c42f52d 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 55340b288d23736d0d514b6089186eb705bda40d..7a7b1b25d56460d9600a2462fbc1f0b38cc49dd2 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 0417f4d5c31c88fb7bde5ec3620aecdada871a33..c64b78b42d0c66a04811a8d73c495b3391677218 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 fe5762e157d97db1da57b23ac857f4d111b3482f..a1ac6afa9ad4cade781c71f184ac01d88984ab73 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 b46f36ca8acbd5e1cf5aaf9c0a7198fc31bd59e0..e571b4fc2cce83e61a9d3f99da28c56e0219ce79 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 a80625768fac4e994fe0a0474c1a9c49df58afb0..78b8c7b8aa18c2c5a17fd72a2676a229852a0754 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 b1b2521268f1a63cbdab716cff1a487867dc4a9c..712b34468831a3e10cca1ff6bcd086bd32b3692c 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 8ce55b8c1efb6a863e4adbcb0d84f7db4de7bd27..d0b9a9657e2c615dad9eaae6835cce059b2f024d 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 6a7a2b81e80674e022db315eaea11a9284b6ca84..a5bd933b1bcfeaffaa80b436a76fac246c85eddb 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 3cb90f7aac4b67754514a1b166a8e0617605aa87..68842329caa54bde292887e7f660019aa75204a9 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 aff929f01af2b43c36b66626dd8e5ca12a4d9576..ad44942e79c58b466fce26436dad805a9512eab4 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 299ef52752ed8594616607474aaddef4bc35ebe1..d37ff58f250004ef4d1fb0e0262f230040f9f336 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 ebe14ffdae03bdf28c428c6be9c0580c661ce305..7f6f4e1316280036e5df8c8d578bbb2b5e487f1b 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 736fa74fbf85b4147c873da56bd003271cd63730..bd126749ac28da329e21c30afd6113528bb91909 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 b0856e556ee84230cff8be109455255cf158f986..82cb1e098dcda026410bc2a0a3703518227ddfac 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 76498068b73e8313c3096f7621c291b9d72f8f79..1f25e6893d061ae45ba834ecb380c4a3d8acfdb3 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 221fdfb3bc9174910217852b81d8f96d1b19a713..3489aa287459e7a28ac2466a765b8a28f44a3e89 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 7d5d683720a246b549814285dd7d10c06b54d586..c15cbee10c3bd49b6bdb5e70c103a1ebac5cb9ff 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 cfc85d0a9b785451261c72d100337868dc307269..5cd9f57c585ba881735715218f8d80be0aab2e2d 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 e0ce794b3c57c0720ecf99a465a0af19e580c703..7d8d28eb790f018916ce262e1b7e0edf862b4c89 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 dca6dab77af85b269ae738a7b0560be789294e31..86f77567c02d0caf7aab6020ddf1b5cb07631098 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 c931af606d284c8aa5c2109b80eebc701a9004c9..9a6fb8012b0a3107d34e7c4cc2c8de9d47b70141 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 d0d733d8c658a55cfeafcbee29b99655a3a0471f..e73a38c074fdf04dbda90f7e6ef41eaca850a587 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);