diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 7a295a841fb35888c817f9dcf5d29ca3a50d0d8a..b325350326a599235c7b2031af3a988c2ca7be80 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -382,7 +382,7 @@ let warn kf name hyp_computer =
| None -> ()
| Some bhv ->
Wp_parameters.warning
- ~current:false ~once:true (* ~source:(fst(Kernel_function.get_location kf)) *)
+ ~current:false ~once:true ~source:(fst(Kernel_function.get_location kf))
"@[<hv 0>Memory model hypotheses for function '%s':@ %t@]"
(Kernel_function.get_name kf)
(print_memory_context kf bhv)
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 b8ebbadea5ebd5ac1be8e37f157226b201709da2..85d0655b52c9c6f00e321eba103e7d31330535af 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
@@ -97,7 +97,8 @@ Effect at line 20
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_acsl/assigns_path.i:12: Warning:
+ Memory model hypotheses for function 'job':
/*@ behavior 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 f318abf289fadf2fa603a1f23a2c77466a989011..cb505e19fd91db51fd8c8581d8930518c446386f 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
@@ -1876,7 +1876,8 @@ Goal Positivity of Loop variant at loop (file tests/wp_acsl/chunk_typing.i, line
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'function':
+[wp] tests/wp_acsl/chunk_typing.i:21: Warning:
+ Memory model hypotheses for function 'function':
/*@
behavior typed:
requires \separated(i16 + (..), (char const *)x + (..));
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 4339266bbaf17b0b122e18a85903f672b452e038..193a70bc4bfe20e9e1f0a2ff6b6a970071934ab1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
@@ -234,11 +234,13 @@ Goal Post-condition 'qed_ko,Eq_oracle_ko' in 'pointer':
Prove: false.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'compare':
+[wp] tests/wp_acsl/pointer.i:63: Warning:
+ Memory model hypotheses for function 'compare':
/*@ behavior typed:
requires \separated(q + (..), &p); */
void compare(int *q);
-[wp] Warning: Memory model hypotheses for function 'absurd':
+[wp] tests/wp_acsl/pointer.i:73: Warning:
+ Memory model hypotheses for function 'absurd':
/*@ behavior 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 180d946c3170c9be3b7dfdaa9a4df4820f951158..d05bde7cc8411f65f2c876e5fc58b7a4d0909523 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
@@ -19,7 +19,8 @@
Functions WP Alt-Ergo Total Success
job 6 3 9 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_acsl/assigns_path.i:12: Warning:
+ Memory model hypotheses for function 'job':
/*@ behavior 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 48e98d4fa14c783c2f68c1b0a33ea97593912457..f5f8f9ccd569d3afe1f92d928c09cb6f971f37c9 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
@@ -49,7 +49,8 @@
Functions WP Alt-Ergo Total Success
function 20 19 39 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'function':
+[wp] tests/wp_acsl/chunk_typing.i:21: Warning:
+ Memory model hypotheses for function 'function':
/*@
behavior typed:
requires \separated(i16 + (..), (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 9e0fd3122c659339481553df508465ea91fdba64..5dee9e18dea7a397b0b68dd1166c5017a69e42f6 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
@@ -26,7 +26,8 @@
mixed_array_pointer - - 2 0.0%
absurd - - 2 0.0%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'absurd':
+[wp] tests/wp_acsl/pointer.i:73: Warning:
+ Memory model hypotheses for function 'absurd':
/*@ behavior 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 5e0172dd87d30107441b9959cdf9c1f5460443b4..60898d58685b7b6774435259868746d719fa009a 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
@@ -26,7 +26,8 @@
mixed_array_pointer - - 2 0.0%
absurd - - 2 0.0%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'absurd':
+[wp] tests/wp_acsl/pointer.i:73: Warning:
+ Memory model hypotheses for function 'absurd':
/*@ behavior 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 8c6fd6aed1b7c5243665509741e7e24b10b1b1d3..65fbcabad5f6feb716502491e09692950ecd13ca 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
@@ -52,7 +52,8 @@ Goal Instance of 'Pre-condition (file tests/wp_bts/bts0843.i, line 12) in 'f3''
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f3':
+[wp] tests/wp_bts/bts0843.i:13: Warning:
+ Memory model hypotheses for function 'f3':
/*@ behavior 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 640c9952226375d9ac25aa5260796f23f8a44c67..ebbd70f4cdb5c0ab25cbdbe4851fd25508a7ad74 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
@@ -65,7 +65,8 @@ Assume {
Prove: global(L_two_24) != one_0.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_frame':
+[wp] tests/wp_bts/bts_1828.i:56: Warning:
+ Memory model hypotheses for function 'global_frame':
/*@ behavior 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 5b00c3b48f392cf59718f82003f6f14f9c6376d4..fdf25268ad263c656d0595867530283b170c00b0 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
@@ -44,7 +44,8 @@ Assume {
Prove: global(L_two_24) != one_0.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_frame':
+[wp] tests/wp_bts/bts_1828.i:56: Warning:
+ Memory model hypotheses for function 'global_frame':
/*@
behavior typed_ref:
requires \separated(zero, one);
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 fbd210f679cb91ec29196a1b2f0e5f4b01f8f764..a522bf115dd4084100bbd4a728c2407f844dd3ca 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
@@ -15,7 +15,8 @@
f3 1 - 1 100%
g3 1 2 3 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f3':
+[wp] tests/wp_bts/bts0843.i:13: Warning:
+ Memory model hypotheses for function 'f3':
/*@ behavior 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 91203bd8a7c316be36b9377c010047ff59f965b9..9bffe58d0b5888097457e33f13a614c0923d1380 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
@@ -17,7 +17,8 @@
local_frame - 1 1 100%
global_frame 3 - 5 60.0%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_frame':
+[wp] tests/wp_bts/bts_1828.i:56: Warning:
+ Memory model hypotheses for function 'global_frame':
/*@ behavior 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 e5edde37e9b7b942c93989d95bb6fd04d5118460..c85bac0087bbe0e5464f4eb837e7ffb174497af5 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
@@ -17,7 +17,8 @@
local_frame - 1 1 100%
global_frame 5 - 5 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_frame':
+[wp] tests/wp_bts/bts_1828.i:56: Warning:
+ Memory model hypotheses for function 'global_frame':
/*@
behavior typed_ref:
requires \separated(zero, one);
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 e21f8f5fe4bc97954c318b6c4531baf28e311bc2..d44fe2c4e6cf3b831856e5f9a29033424f325831 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
@@ -52,7 +52,8 @@
[wp] Goal typed_ref_equal_elements_loop_variant_positive : not tried
[wp] Goal typed_ref_equal_elements_loop_variant_2_decrease : not tried
[wp] Goal typed_ref_equal_elements_loop_variant_2_positive : not tried
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
+[wp] tests/wp_gallery/frama_c_exo3_solved.old.c:73: Warning:
+ Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
requires \separated(v1, v2, a + (..));
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 0a5004c676571d4ea94cd0cf4e06b37217771f29..68e0c5d7ad61be97d82deb34c0685928eccfe3ab 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
@@ -53,7 +53,8 @@
[wp] Goal typed_ref_equal_elements_loop_variant_positive : not tried
[wp] Goal typed_ref_equal_elements_loop_variant_2_decrease : not tried
[wp] Goal typed_ref_equal_elements_loop_variant_2_positive : not tried
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
+[wp] tests/wp_gallery/frama_c_exo3_solved.old.v2.c:56: Warning:
+ Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
requires \separated(v1, v2, a + (..));
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 920eb2e7847aef95800fe191f9b6ea0c867c74db..70ff1ce19f1e4c50cb97c8ec8ae310d3df64c9ba 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
@@ -44,7 +44,8 @@
Functions WP Alt-Ergo Total Success
equal_elements 18 16 34 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
+[wp] tests/wp_gallery/frama_c_exo3_solved.old.c:73: Warning:
+ Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
requires \separated(v1, v2, a + (..));
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 86908f16b544470cc8ec005ac807a83ad595dd8a..a87e532706dc3c93fcf82afc8e891eb1e836b190 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
@@ -45,7 +45,8 @@
Functions WP Alt-Ergo Total Success
equal_elements 17 18 35 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
+[wp] tests/wp_gallery/frama_c_exo3_solved.old.v2.c:56: Warning:
+ Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
requires \separated(v1, v2, a + (..));
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 832baab84eb61db255327ed172594084b92caa0c..793f91fafc8b11ae56f885196d13c202f7031b25 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
@@ -193,49 +193,57 @@ Effect at line 103
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:17: Warning:
+ Memory model hypotheses for function 'global_alias':
/*@
behavior typed:
requires \separated(g_alias, (int *)global + (..), &g_alias);
*/
void global_alias(void);
-[wp] Warning: Memory model hypotheses for function 'global_no_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:24: Warning:
+ Memory model hypotheses for function 'global_no_alias':
/*@ behavior typed:
requires \separated(g_alias, &g_alias); */
void global_no_alias(void);
-[wp] Warning: Memory model hypotheses for function 'formal_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:32: Warning:
+ Memory model hypotheses for function 'formal_alias':
/*@ behavior typed:
requires \separated(f_alias, (int *)global + (..)); */
void formal_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:48: Warning:
+ Memory model hypotheses for function 'formal_alias_array':
/*@
behavior typed:
requires \separated((int *)global + (..), &(*alias_array)[0 .. 1]);
requires \separated(alias_array + (..), (int *)global + (..));
*/
void formal_alias_array(int (*alias_array)[2]);
-[wp] Warning: Memory model hypotheses for function 'field_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:61: Warning:
+ Memory model hypotheses for function 'field_alias':
/*@
behavior typed:
requires \separated((int *)global + (..), &x->x);
requires \separated(x, (int *)global + (..));
*/
void field_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'field_range_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:73: Warning:
+ Memory model hypotheses for function 'field_range_alias':
/*@
behavior typed:
requires \separated((int *)global + (..), &(x + (0 .. 3))->x);
requires \separated(x + (..), (int *)global + (..));
*/
void field_range_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'set_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:81: Warning:
+ Memory model hypotheses for function 'set_alias':
/*@
behavior typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
*/
void set_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:92: Warning:
+ Memory model hypotheses for function 'comprehension_alias':
/*@
behavior typed:
requires
@@ -245,7 +253,8 @@ Prove: true.
);
*/
void comprehension_alias(void);
-[wp] Warning: Memory model hypotheses for function 'union_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:102: Warning:
+ Memory model hypotheses for function 'union_alias':
/*@
behavior typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
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 54ad8489278e68186e342fc1157d755cd613d62f..1fa158d4b18a42536b46fc8d617c79c8addd69dc 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
@@ -85,15 +85,18 @@ Goal Instance of 'Pre-condition (file tests/wp_hoare/byref.i, line 11) in 'f'' i
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_hoare/byref.i:14: Warning:
+ Memory model hypotheses for function 'f':
/*@ behavior typed_ref:
requires \valid(r); */
void f(int *r);
-[wp] Warning: Memory model hypotheses for function 'wrong_without_ref':
+[wp] tests/wp_hoare/byref.i:20: Warning:
+ Memory model hypotheses for function 'wrong_without_ref':
/*@ behavior typed_ref:
requires \valid(q); */
int wrong_without_ref(int *q);
-[wp] Warning: Memory model hypotheses for function 'pointer':
+[wp] tests/wp_hoare/byref.i:31: Warning:
+ Memory model hypotheses for function 'pointer':
/*@ behavior 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 a331a12473931391078fc0c740594fe6d94275fa..3b0db52682911a8d6ab8cc90fdf69221793feba4 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
@@ -496,19 +496,23 @@ Effect at line 46
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'ref_ctr':
+[wp] tests/wp_hoare/dispatch_var.i:12: Warning:
+ Memory model hypotheses for function 'ref_ctr':
/*@ behavior typed_ref:
requires \valid(p); */
int ref_ctr(int *p);
-[wp] Warning: Memory model hypotheses for function 'ref_bd':
+[wp] tests/wp_hoare/dispatch_var.i:44: Warning:
+ Memory model hypotheses for function 'ref_bd':
/*@ behavior typed_ref:
requires \valid(q); */
int ref_bd(int *q);
-[wp] Warning: Memory model hypotheses for function 'ref_valid':
+[wp] tests/wp_hoare/dispatch_var.i:83: Warning:
+ Memory model hypotheses for function 'ref_valid':
/*@ behavior typed_ref:
requires \valid(p1); */
int ref_valid(int *p1);
-[wp] Warning: Memory model hypotheses for function 'ref_ctr_nr':
+[wp] tests/wp_hoare/dispatch_var.i:133: Warning:
+ Memory model hypotheses for function 'ref_ctr_nr':
/*@
behavior typed_ref:
requires \separated(ref, ref1, ref2);
@@ -517,11 +521,13 @@ Prove: true.
requires \valid(ref2);
*/
int ref_ctr_nr(int *ref, int *ref1, int *ref2);
-[wp] Warning: Memory model hypotheses for function 'ref_ctr_nstars':
+[wp] tests/wp_hoare/dispatch_var.i:158: Warning:
+ Memory model hypotheses for function 'ref_ctr_nstars':
/*@ behavior typed_ref:
requires \valid(pp); */
int ref_ctr_nstars(int **pp);
-[wp] Warning: Memory model hypotheses for function 'g':
+[wp] tests/wp_hoare/dispatch_var.i:194: Warning:
+ Memory model hypotheses for function 'g':
/*@ behavior 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 61bf6b67367b214b40e53f5d9d9e9fff16e4a0fe..9920ee4d4ce39ff13cde465cd8e8a4e73071e3e1 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
@@ -485,19 +485,23 @@ Goal Assigns (file tests/wp_hoare/dispatch_var2.i, line 13) in 'reset':
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
+[wp] tests/wp_hoare/dispatch_var2.i:16: Warning:
+ Memory model hypotheses for function 'reset':
/*@ behavior typed_ref:
requires \valid(rp); */
void reset(int *rp);
-[wp] Warning: Memory model hypotheses for function 'incr':
+[wp] tests/wp_hoare/dispatch_var2.i:23: Warning:
+ Memory model hypotheses for function 'incr':
/*@ behavior typed_ref:
requires \valid(ip); */
void incr(int *ip);
-[wp] Warning: Memory model hypotheses for function 'load':
+[wp] tests/wp_hoare/dispatch_var2.i:31: Warning:
+ Memory model hypotheses for function 'load':
/*@ behavior typed_ref:
requires \valid(lp); */
int load(int *lp);
-[wp] Warning: Memory model hypotheses for function 'call_param_ref':
+[wp] tests/wp_hoare/dispatch_var2.i:70: Warning:
+ Memory model hypotheses for function 'call_param_ref':
/*@ behavior 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 44ae58e7b74ba0fb1e7c7ef27a28f0155be239f7..932c183de67c2c15fac39260964ad91f34d3e149 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
@@ -210,19 +210,23 @@ Goal Assigns (file tests/wp_hoare/dispatch_var2.i, line 13) in 'reset':
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
+[wp] tests/wp_hoare/dispatch_var2.i:16: Warning:
+ Memory model hypotheses for function 'reset':
/*@ behavior typed_ref:
requires \valid(rp); */
void reset(int *rp);
-[wp] Warning: Memory model hypotheses for function 'incr':
+[wp] tests/wp_hoare/dispatch_var2.i:23: Warning:
+ Memory model hypotheses for function 'incr':
/*@ behavior typed_ref:
requires \valid(ip); */
void incr(int *ip);
-[wp] Warning: Memory model hypotheses for function 'load':
+[wp] tests/wp_hoare/dispatch_var2.i:31: Warning:
+ Memory model hypotheses for function 'load':
/*@ behavior typed_ref:
requires \valid(lp); */
int load(int *lp);
-[wp] Warning: Memory model hypotheses for function 'call_param_ref':
+[wp] tests/wp_hoare/dispatch_var2.i:70: Warning:
+ Memory model hypotheses for function 'call_param_ref':
/*@ behavior 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 3b23754654d105529aebf67dfd10ca1a458a5953..c7395b1a724d5c497e330ed30c33d8df230504aa 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
@@ -141,11 +141,13 @@ Goal Assigns (file tests/wp_hoare/reference.i, line 57) in 'write':
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_hoare/reference.i:14: Warning:
+ Memory model hypotheses for function 'f':
/*@ behavior typed_ref:
requires \valid(p); */
int f(int *p);
-[wp] Warning: Memory model hypotheses for function 'f2':
+[wp] tests/wp_hoare/reference.i:30: Warning:
+ Memory model hypotheses for function 'f2':
/*@
behavior typed_ref:
requires \separated(p2, q);
@@ -153,15 +155,18 @@ Prove: true.
requires \valid(q);
*/
int f2(int *p2, int *q);
-[wp] Warning: Memory model hypotheses for function 'call_f2':
+[wp] tests/wp_hoare/reference.i:37: Warning:
+ Memory model hypotheses for function 'call_f2':
/*@ behavior typed_ref:
requires \valid(ptr); */
int call_f2(int *ptr, int y);
-[wp] Warning: Memory model hypotheses for function 'call_global':
+[wp] tests/wp_hoare/reference.i:48: Warning:
+ Memory model hypotheses for function 'call_global':
/*@ behavior typed_ref:
requires \valid(gl); */
int call_global(void);
-[wp] Warning: Memory model hypotheses for function 'write':
+[wp] tests/wp_hoare/reference.i:60: Warning:
+ Memory model hypotheses for function 'write':
/*@ behavior 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 fc78cf9e70fb096b7323945a45a606e3f5a12343..f816e6df044db643780fcfefb4a18db78d8d6ee4 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
@@ -251,17 +251,20 @@ Goal Assigns (file tests/wp_hoare/reference_and_struct.i, line 12) in 'reset':
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
+[wp] tests/wp_hoare/reference_and_struct.i:15: Warning:
+ Memory model hypotheses for function 'reset':
/*@ behavior typed_ref:
requires \valid(p); */
void reset(struct T *p);
-[wp] Warning: Memory model hypotheses for function 'call_reset_5_tps':
+[wp] tests/wp_hoare/reference_and_struct.i:48: Warning:
+ Memory model hypotheses for function 'call_reset_5_tps':
/*@
behavior typed_ref:
requires \separated((struct T **)tps + (..), tps[9] + (0 .. 4));
*/
void call_reset_5_tps(void);
-[wp] Warning: Memory model hypotheses for function 'load_5':
+[wp] tests/wp_hoare/reference_and_struct.i:88: Warning:
+ Memory model hypotheses for function 'load_5':
/*@
behavior typed_ref:
requires \separated(hp + (..), (int *)reg_load + (..));
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 bc9d8f6a5c0f8575b970c7583b00a16b25556dd1..fe649246798c8210ee07cd60014b3b8020249e24 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
@@ -401,26 +401,30 @@ Goal Instance of 'Pre-condition (file tests/wp_hoare/reference_array.i, line 9)
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'load_5':
+[wp] tests/wp_hoare/reference_array.i:24: Warning:
+ Memory model hypotheses for function 'load_5':
/*@
behavior typed_ref:
requires \separated(hp + (..), (int *)reg_load + (..));
*/
void load_5(int *hp);
-[wp] Warning: Memory model hypotheses for function 'add_5':
+[wp] tests/wp_hoare/reference_array.i:31: Warning:
+ Memory model hypotheses for function 'add_5':
/*@
behavior typed_ref:
requires
\separated(gp + (..), (int *)reg_load + (..), (int *)reg_add + (..));
*/
void add_5(int *gp);
-[wp] Warning: Memory model hypotheses for function 'load_1_5':
+[wp] tests/wp_hoare/reference_array.i:45: Warning:
+ Memory model hypotheses for function 'load_1_5':
/*@
behavior typed_ref:
requires \separated(lp + (..), (int *)reg_load + (..));
*/
void load_1_5(int (*lp)[5]);
-[wp] Warning: Memory model hypotheses for function 'add_1_5':
+[wp] tests/wp_hoare/reference_array.i:52: Warning:
+ Memory model hypotheses for function 'add_1_5':
/*@
behavior typed_ref:
requires
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 59c0568ee15ab1f2f1a4475f688e303403a07b4b..bb63bebf59aac3371d4afd549278466915ae84f5 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
@@ -68,7 +68,8 @@ Assume { (* Heap *) Type: (region(c.base) <= 0) /\ (region(d.base) <= 0). }
Prove: d != c.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_hoare/refguards.i:10: Warning:
+ Memory model hypotheses for function 'f':
/*@
behavior typed_ref:
requires \separated(c, d, {a + (..), b + (..)});
@@ -76,7 +77,8 @@ Prove: d != c.
requires \valid(d);
*/
void f(int *a, int *b, int *c, int *d, int k);
-[wp] Warning: Memory model hypotheses for function 'h':
+[wp] tests/wp_hoare/refguards.i:25: Warning:
+ Memory model hypotheses for function 'h':
/*@
behavior typed_ref:
requires \separated(c, d);
@@ -84,7 +86,8 @@ Prove: d != c.
requires \valid(d);
*/
void h(int *c, int *d, int k);
-[wp] Warning: Memory model hypotheses for function 's':
+[wp] tests/wp_hoare/refguards.i:39: Warning:
+ Memory model hypotheses for function 's':
/*@
behavior typed_ref:
requires \separated(c, 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 33a25d793ff22746cb810bbf039b5d65e0bc4bf5..99cd98673ce8c30cb84f9b4592bd0be80b8c2d4b 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
@@ -48,49 +48,57 @@
comprehension_alias 3 - 3 100%
union_alias 3 - 3 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:17: Warning:
+ Memory model hypotheses for function 'global_alias':
/*@
behavior typed:
requires \separated(g_alias, (int *)global + (..), &g_alias);
*/
void global_alias(void);
-[wp] Warning: Memory model hypotheses for function 'global_no_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:24: Warning:
+ Memory model hypotheses for function 'global_no_alias':
/*@ behavior typed:
requires \separated(g_alias, &g_alias); */
void global_no_alias(void);
-[wp] Warning: Memory model hypotheses for function 'formal_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:32: Warning:
+ Memory model hypotheses for function 'formal_alias':
/*@ behavior typed:
requires \separated(f_alias, (int *)global + (..)); */
void formal_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:48: Warning:
+ Memory model hypotheses for function 'formal_alias_array':
/*@
behavior typed:
requires \separated((int *)global + (..), &(*alias_array)[0 .. 1]);
requires \separated(alias_array + (..), (int *)global + (..));
*/
void formal_alias_array(int (*alias_array)[2]);
-[wp] Warning: Memory model hypotheses for function 'field_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:61: Warning:
+ Memory model hypotheses for function 'field_alias':
/*@
behavior typed:
requires \separated((int *)global + (..), &x->x);
requires \separated(x, (int *)global + (..));
*/
void field_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'field_range_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:73: Warning:
+ Memory model hypotheses for function 'field_range_alias':
/*@
behavior typed:
requires \separated((int *)global + (..), &(x + (0 .. 3))->x);
requires \separated(x + (..), (int *)global + (..));
*/
void field_range_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'set_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:81: Warning:
+ Memory model hypotheses for function 'set_alias':
/*@
behavior typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
*/
void set_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:92: Warning:
+ Memory model hypotheses for function 'comprehension_alias':
/*@
behavior typed:
requires
@@ -100,7 +108,8 @@
);
*/
void comprehension_alias(void);
-[wp] Warning: Memory model hypotheses for function 'union_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:102: Warning:
+ Memory model hypotheses for function 'union_alias':
/*@
behavior typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_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 48e1936e19564287ad810f53ddca2ccc7767dc19..816e897df18e973f7469fde30c0b26c8d9cc67ef 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
@@ -26,15 +26,18 @@
formal 2 - 2 100%
global 2 - 2 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_hoare/byref.i:14: Warning:
+ Memory model hypotheses for function 'f':
/*@ behavior typed_ref:
requires \valid(r); */
void f(int *r);
-[wp] Warning: Memory model hypotheses for function 'wrong_without_ref':
+[wp] tests/wp_hoare/byref.i:20: Warning:
+ Memory model hypotheses for function 'wrong_without_ref':
/*@ behavior typed_ref:
requires \valid(q); */
int wrong_without_ref(int *q);
-[wp] Warning: Memory model hypotheses for function 'pointer':
+[wp] tests/wp_hoare/byref.i:31: Warning:
+ Memory model hypotheses for function 'pointer':
/*@ behavior 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 c2c4c3b968309e4b7bcdc2213826182aeaa243a8..aa66d23b2fc824f2a9fcc290903ad10e2472f60b 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
@@ -99,19 +99,23 @@
g 4 - 4 100%
array_in_struct_param 2 - 2 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'ref_ctr':
+[wp] tests/wp_hoare/dispatch_var.i:12: Warning:
+ Memory model hypotheses for function 'ref_ctr':
/*@ behavior typed_ref:
requires \valid(p); */
int ref_ctr(int *p);
-[wp] Warning: Memory model hypotheses for function 'ref_bd':
+[wp] tests/wp_hoare/dispatch_var.i:44: Warning:
+ Memory model hypotheses for function 'ref_bd':
/*@ behavior typed_ref:
requires \valid(q); */
int ref_bd(int *q);
-[wp] Warning: Memory model hypotheses for function 'ref_valid':
+[wp] tests/wp_hoare/dispatch_var.i:83: Warning:
+ Memory model hypotheses for function 'ref_valid':
/*@ behavior typed_ref:
requires \valid(p1); */
int ref_valid(int *p1);
-[wp] Warning: Memory model hypotheses for function 'ref_ctr_nr':
+[wp] tests/wp_hoare/dispatch_var.i:133: Warning:
+ Memory model hypotheses for function 'ref_ctr_nr':
/*@
behavior typed_ref:
requires \separated(ref, ref1, ref2);
@@ -120,11 +124,13 @@
requires \valid(ref2);
*/
int ref_ctr_nr(int *ref, int *ref1, int *ref2);
-[wp] Warning: Memory model hypotheses for function 'ref_ctr_nstars':
+[wp] tests/wp_hoare/dispatch_var.i:158: Warning:
+ Memory model hypotheses for function 'ref_ctr_nstars':
/*@ behavior typed_ref:
requires \valid(pp); */
int ref_ctr_nstars(int **pp);
-[wp] Warning: Memory model hypotheses for function 'g':
+[wp] tests/wp_hoare/dispatch_var.i:194: Warning:
+ Memory model hypotheses for function 'g':
/*@ behavior 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 b5878139820eb2eed4ceb79df18a6690a4635426..9172fe5d07b12a7013a117e077c9c88d97db1c53 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
@@ -49,19 +49,23 @@
call_local 8 - 8 100%
call_param_ref 6 - 6 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
+[wp] tests/wp_hoare/dispatch_var2.i:16: Warning:
+ Memory model hypotheses for function 'reset':
/*@ behavior typed_ref:
requires \valid(rp); */
void reset(int *rp);
-[wp] Warning: Memory model hypotheses for function 'incr':
+[wp] tests/wp_hoare/dispatch_var2.i:23: Warning:
+ Memory model hypotheses for function 'incr':
/*@ behavior typed_ref:
requires \valid(ip); */
void incr(int *ip);
-[wp] Warning: Memory model hypotheses for function 'load':
+[wp] tests/wp_hoare/dispatch_var2.i:31: Warning:
+ Memory model hypotheses for function 'load':
/*@ behavior typed_ref:
requires \valid(lp); */
int load(int *lp);
-[wp] Warning: Memory model hypotheses for function 'call_param_ref':
+[wp] tests/wp_hoare/dispatch_var2.i:70: Warning:
+ Memory model hypotheses for function 'call_param_ref':
/*@ behavior 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 7a50ede52eb9de48083e80185e8fbe5291b9697e..26521bbd90e8db80954e4a8e6971f3297d08abc0 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
@@ -49,19 +49,23 @@
call_local 8 - 8 100%
call_param_ref 6 - 6 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
+[wp] tests/wp_hoare/dispatch_var2.i:16: Warning:
+ Memory model hypotheses for function 'reset':
/*@ behavior typed_ref:
requires \valid(rp); */
void reset(int *rp);
-[wp] Warning: Memory model hypotheses for function 'incr':
+[wp] tests/wp_hoare/dispatch_var2.i:23: Warning:
+ Memory model hypotheses for function 'incr':
/*@ behavior typed_ref:
requires \valid(ip); */
void incr(int *ip);
-[wp] Warning: Memory model hypotheses for function 'load':
+[wp] tests/wp_hoare/dispatch_var2.i:31: Warning:
+ Memory model hypotheses for function 'load':
/*@ behavior typed_ref:
requires \valid(lp); */
int load(int *lp);
-[wp] Warning: Memory model hypotheses for function 'call_param_ref':
+[wp] tests/wp_hoare/dispatch_var2.i:70: Warning:
+ Memory model hypotheses for function 'call_param_ref':
/*@ behavior 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 293e74343d6730671635c5d81fb109e7b6dae34a..f90e23c73a56d68a5670142e2331b020f91fdff6 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
@@ -36,11 +36,13 @@
call_global 5 - 5 100%
write 2 - 2 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_hoare/reference.i:14: Warning:
+ Memory model hypotheses for function 'f':
/*@ behavior typed_ref:
requires \valid(p); */
int f(int *p);
-[wp] Warning: Memory model hypotheses for function 'f2':
+[wp] tests/wp_hoare/reference.i:30: Warning:
+ Memory model hypotheses for function 'f2':
/*@
behavior typed_ref:
requires \separated(p2, q);
@@ -48,15 +50,18 @@
requires \valid(q);
*/
int f2(int *p2, int *q);
-[wp] Warning: Memory model hypotheses for function 'call_f2':
+[wp] tests/wp_hoare/reference.i:37: Warning:
+ Memory model hypotheses for function 'call_f2':
/*@ behavior typed_ref:
requires \valid(ptr); */
int call_f2(int *ptr, int y);
-[wp] Warning: Memory model hypotheses for function 'call_global':
+[wp] tests/wp_hoare/reference.i:48: Warning:
+ Memory model hypotheses for function 'call_global':
/*@ behavior typed_ref:
requires \valid(gl); */
int call_global(void);
-[wp] Warning: Memory model hypotheses for function 'write':
+[wp] tests/wp_hoare/reference.i:60: Warning:
+ Memory model hypotheses for function 'write':
/*@ behavior 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 61dba2feb73e235a1e40221abdee6909be09a308..48133b9d6ee5bb8492567fd1e13d61fd9825ecab 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
@@ -49,17 +49,20 @@
call_on_array_in_struct_global 3 1 4 100%
call_array_in_struct_param 5 - 5 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
+[wp] tests/wp_hoare/reference_and_struct.i:15: Warning:
+ Memory model hypotheses for function 'reset':
/*@ behavior typed_ref:
requires \valid(p); */
void reset(struct T *p);
-[wp] Warning: Memory model hypotheses for function 'call_reset_5_tps':
+[wp] tests/wp_hoare/reference_and_struct.i:48: Warning:
+ Memory model hypotheses for function 'call_reset_5_tps':
/*@
behavior typed_ref:
requires \separated((struct T **)tps + (..), tps[9] + (0 .. 4));
*/
void call_reset_5_tps(void);
-[wp] Warning: Memory model hypotheses for function 'load_5':
+[wp] tests/wp_hoare/reference_and_struct.i:88: Warning:
+ Memory model hypotheses for function 'load_5':
/*@
behavior typed_ref:
requires \separated(hp + (..), (int *)reg_load + (..));
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 67a8d5d5f1489613b0a59ade15cc6214b121278d..4a84b4eb4b8c8afb7e12d1857d5493d093e7bd80 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
@@ -51,26 +51,30 @@
calls_on_array_dim_2_to_1 5 3 8 100%
calls_on_array_dim_2 5 3 8 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'load_5':
+[wp] tests/wp_hoare/reference_array.i:24: Warning:
+ Memory model hypotheses for function 'load_5':
/*@
behavior typed_ref:
requires \separated(hp + (..), (int *)reg_load + (..));
*/
void load_5(int *hp);
-[wp] Warning: Memory model hypotheses for function 'add_5':
+[wp] tests/wp_hoare/reference_array.i:31: Warning:
+ Memory model hypotheses for function 'add_5':
/*@
behavior typed_ref:
requires
\separated(gp + (..), (int *)reg_load + (..), (int *)reg_add + (..));
*/
void add_5(int *gp);
-[wp] Warning: Memory model hypotheses for function 'load_1_5':
+[wp] tests/wp_hoare/reference_array.i:45: Warning:
+ Memory model hypotheses for function 'load_1_5':
/*@
behavior typed_ref:
requires \separated(lp + (..), (int *)reg_load + (..));
*/
void load_1_5(int (*lp)[5]);
-[wp] Warning: Memory model hypotheses for function 'add_1_5':
+[wp] tests/wp_hoare/reference_array.i:52: Warning:
+ Memory model hypotheses for function 'add_1_5':
/*@
behavior typed_ref:
requires
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 02a4bffe2c4d64132a21a44142ddcf9bf1b3f99f..9a42e6480755beabc8ff4e171354431611c8e39a 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
@@ -22,7 +22,8 @@
h 1 - 1 100%
s 5 - 6 83.3%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_hoare/refguards.i:10: Warning:
+ Memory model hypotheses for function 'f':
/*@
behavior typed_ref:
requires \separated(c, d, {a + (..), b + (..)});
@@ -30,7 +31,8 @@
requires \valid(d);
*/
void f(int *a, int *b, int *c, int *d, int k);
-[wp] Warning: Memory model hypotheses for function 'h':
+[wp] tests/wp_hoare/refguards.i:25: Warning:
+ Memory model hypotheses for function 'h':
/*@
behavior typed_ref:
requires \separated(c, d);
@@ -38,7 +40,8 @@
requires \valid(d);
*/
void h(int *c, int *d, int k);
-[wp] Warning: Memory model hypotheses for function 's':
+[wp] tests/wp_hoare/refguards.i:39: Warning:
+ Memory model hypotheses for function 's':
/*@
behavior typed_ref:
requires \separated(c, 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 e71c6e9ae9aea0d46a37b93de7f0bd295d0e1fb5..91365d446b74714bc8e525b1a263f63b68ea802e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -372,19 +372,23 @@ Tags: Call h1.
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'guarded_call':
+[wp] tests/wp_plugin/dynamic.i:41: Warning:
+ Memory model hypotheses for function 'guarded_call':
/*@ behavior typed:
requires \separated(p, &X); */
void guarded_call(struct S *p);
-[wp] Warning: Memory model hypotheses for function 'behavior':
+[wp] tests/wp_plugin/dynamic.i:63: Warning:
+ Memory model hypotheses for function 'behavior':
/*@ behavior typed:
requires \separated(p + (..), &X1); */
int behavior(int (*p)(void));
-[wp] Warning: Memory model hypotheses for function 'some_behaviors':
+[wp] tests/wp_plugin/dynamic.i:76: Warning:
+ Memory model hypotheses for function 'some_behaviors':
/*@ behavior typed:
requires \separated(p + (..), &X1); */
int some_behaviors(int (*p)(void));
-[wp] Warning: Memory model hypotheses for function 'missing_context':
+[wp] tests/wp_plugin/dynamic.i:85: Warning:
+ Memory model hypotheses for function 'missing_context':
/*@ behavior 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 a3bcc315fdac6c66cfa7881ddf59d613adc25e89..6f296e1d079de70a596bdd4040d8e4c6ece6ec89 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
@@ -100,11 +100,13 @@ Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), -5), 10).
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f1_ok':
+[wp] tests/wp_plugin/overassign.i:14: Warning:
+ Memory model hypotheses for function 'f1_ok':
/*@ behavior typed:
requires \separated(p + (0 .. 9), &p); */
void f1_ok(void);
-[wp] Warning: Memory model hypotheses for function 'f2_ok':
+[wp] tests/wp_plugin/overassign.i:17: Warning:
+ Memory model hypotheses for function 'f2_ok':
/*@ behavior 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 45299879b14e3dca2096f688d1cba863728a4377..d557391b19112f81757a1ec381d4c8654843220f 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
@@ -32,7 +32,8 @@ Call Effect at line 14
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'receive':
+[wp] tests/wp_plugin/post_assigns.i:12: Warning:
+ Memory model hypotheses for function 'receive':
/*@
behavior typed:
requires \separated(message + (..), &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 fdfb80b6c398acb479a2221181fa65057e0b48bf..61c35549a7f26dec27865a64f21521a7eb2621fe 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
@@ -66,17 +66,20 @@ Goal Post-condition (file tests/wp_plugin/sep.i, line 48) in 'f8_pq_a':
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f2_p_a':
+[wp] tests/wp_plugin/sep.i:18: Warning:
+ Memory model hypotheses for function 'f2_p_a':
/*@ behavior typed_caveat:
requires \separated(p, &a);
requires \valid(p); */
void f2_p_a(int *p);
-[wp] Warning: Memory model hypotheses for function 'f3_p_ab':
+[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); */
void f3_p_ab(int *p);
-[wp] Warning: Memory model hypotheses for function 'f4_pq_ab':
+[wp] tests/wp_plugin/sep.i:26: Warning:
+ Memory model hypotheses for function 'f4_pq_ab':
/*@
behavior typed_caveat:
requires \separated(p, q, &a, &b);
@@ -84,7 +87,8 @@ Prove: true.
requires \valid(q);
*/
void f4_pq_ab(int *p, int *q);
-[wp] Warning: Memory model hypotheses for function 'f5_pq':
+[wp] tests/wp_plugin/sep.i:30: Warning:
+ Memory model hypotheses for function 'f5_pq':
/*@
behavior typed_caveat:
requires \separated(p, q);
@@ -92,14 +96,16 @@ Prove: true.
requires \valid(q);
*/
void f5_pq(int *p, int *q);
-[wp] Warning: Memory model hypotheses for function 'f6_Pa':
+[wp] tests/wp_plugin/sep.i:34: Warning:
+ Memory model hypotheses for function 'f6_Pa':
/*@
behavior typed_caveat:
requires \separated(p + (..), &a);
requires \valid(p + (..));
*/
void f6_Pa(int *p, int k);
-[wp] Warning: Memory model hypotheses for function 'f7_pq_ad':
+[wp] tests/wp_plugin/sep.i:43: Warning:
+ Memory model hypotheses for function 'f7_pq_ad':
/*@
behavior typed_caveat:
requires \separated(p, q, &a, &d);
@@ -107,7 +113,8 @@ Prove: true.
requires \valid(q);
*/
void f7_pq_ad(int *p, int *q);
-[wp] Warning: Memory model hypotheses for function 'f8_pq_a':
+[wp] tests/wp_plugin/sep.i:49: Warning:
+ Memory model hypotheses for function 'f8_pq_a':
/*@
behavior typed_caveat:
requires \separated(p, q, &a);
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 719b55d64916de58d356ed9c4e87832c0af942c2..b43689ed846fb7f49744e7e768079a085efd73fb 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
@@ -42,7 +42,8 @@ Assume {
Prove: valid_rw(Malloc_0, p, 2).
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'fopen':
+[wp] tests/wp_plugin/subset_fopen.c:13: Warning:
+ Memory model hypotheses for function 'fopen':
/*@
behavior typed:
requires \separated(&_p__fc_fopen, {filename + (..), mode + (..)});
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 8f0c8d4ce8a3ca974c104502d4572ad66bf635a6..015937705a8d43b4ee893e04224eaaee149f5f51 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
@@ -35,7 +35,8 @@ Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 35):
Prove: EqS1_st_v(w, w_1).
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job_struct_assigns':
+[wp] tests/wp_plugin/volatile.i:32: Warning:
+ Memory model hypotheses for function 'job_struct_assigns':
/*@ behavior 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 8f7b2282f202b7a6ab2c4fb7f9faa450a8594c32..8736e619bd18aeb73a6fd945870497310334e0a9 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
@@ -69,7 +69,8 @@ tests/wp_plugin/volatile.i:35: warning from wp:
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job_struct_assigns':
+[wp] tests/wp_plugin/volatile.i:32: Warning:
+ Memory model hypotheses for function 'job_struct_assigns':
/*@ behavior 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 9144906c8da84fbc097b34efdbe590b66f253b4a..f2e983f6020cd64b9e459140833506dde59690e1 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
@@ -67,19 +67,23 @@
missing_context 4 - 5 80.0%
no_call 4 - 4 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'guarded_call':
+[wp] tests/wp_plugin/dynamic.i:41: Warning:
+ Memory model hypotheses for function 'guarded_call':
/*@ behavior typed:
requires \separated(p, &X); */
void guarded_call(struct S *p);
-[wp] Warning: Memory model hypotheses for function 'behavior':
+[wp] tests/wp_plugin/dynamic.i:63: Warning:
+ Memory model hypotheses for function 'behavior':
/*@ behavior typed:
requires \separated(p + (..), &X1); */
int behavior(int (*p)(void));
-[wp] Warning: Memory model hypotheses for function 'some_behaviors':
+[wp] tests/wp_plugin/dynamic.i:76: Warning:
+ Memory model hypotheses for function 'some_behaviors':
/*@ behavior typed:
requires \separated(p + (..), &X1); */
int some_behaviors(int (*p)(void));
-[wp] Warning: Memory model hypotheses for function 'missing_context':
+[wp] tests/wp_plugin/dynamic.i:85: Warning:
+ Memory model hypotheses for function 'missing_context':
/*@ behavior 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 5bfb2cf3e3404fc852f21bd6bce54e9d187991a5..48f494c79a7826f0372c9abb423449505d239ab4 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
@@ -27,11 +27,13 @@
f5_ko - - 2 0.0%
f6_ko - - 2 0.0%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f1_ok':
+[wp] tests/wp_plugin/overassign.i:14: Warning:
+ Memory model hypotheses for function 'f1_ok':
/*@ behavior typed:
requires \separated(p + (0 .. 9), &p); */
void f1_ok(void);
-[wp] Warning: Memory model hypotheses for function 'f2_ok':
+[wp] tests/wp_plugin/overassign.i:17: Warning:
+ Memory model hypotheses for function 'f2_ok':
/*@ behavior 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 7333f0d562cc399e0e57a50f1e8658ee0617e787..bde4fe1a2403a2c73bdcb61ae4a868fb1c46b58d 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
@@ -14,7 +14,8 @@
Functions WP Alt-Ergo Total Success
receive 5 - 5 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'receive':
+[wp] tests/wp_plugin/post_assigns.i:12: Warning:
+ Memory model hypotheses for function 'receive':
/*@
behavior typed:
requires \separated(message + (..), &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 9ab32fb6c08820defae09bd643e1b58079344579..14f5f8935ded5f409c4738bb39c355cca1935023 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
@@ -15,7 +15,8 @@
Functions WP Alt-Ergo Total Success
f 3 1 5 80.0%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'fopen':
+[wp] tests/wp_plugin/subset_fopen.c:13: Warning:
+ Memory model hypotheses for function 'fopen':
/*@
behavior typed:
requires \separated(&_p__fc_fopen, {filename + (..), mode + (..)});
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 02cc117a476d17a985f7c1ea62def4751c5ba218..560e614362406b9c7e49ecd5d731746e2ab88397 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
@@ -25,11 +25,13 @@ Assume {
Prove: `x_2 = `x_1.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'get_int':
+[wp] tests/wp_tip/chunk_printing.i:19: Warning:
+ Memory model hypotheses for function 'get_int':
/*@ behavior typed:
requires \separated(v, &y); */
int *get_int(struct V *v);
-[wp] Warning: Memory model hypotheses for function 'get_uint':
+[wp] tests/wp_tip/chunk_printing.i:25: Warning:
+ Memory model hypotheses for function 'get_uint':
/*@ behavior typed:
requires \separated(v, &y); */
unsigned int *get_uint(struct V *v);
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 2394b867cc2f1a53f22cb7f7f457a25835d95ae5..21e31a09591178e574a7787a5a2870513301fd03 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
@@ -18,7 +18,8 @@ Assume {
Prove: P_equal(1, 1).
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'Write':
+[wp] tests/wp_typed/mvar.i:8: Warning:
+ Memory model hypotheses for function 'Write':
/*@
behavior typed:
requires \separated(p + (..), (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 5b2b41742803a0cf26d679e1111ef0a62d344f5e..2c2ed44ef412f4455658321defa7791f181de35e 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
@@ -18,7 +18,8 @@ Assume {
Prove: P_equal(1, 1).
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'Write':
+[wp] tests/wp_typed/mvar.i:8: Warning:
+ Memory model hypotheses for function 'Write':
/*@
behavior typed_ref:
requires \separated(p + (..), (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 498ce46ee4c976e50fbcd1c9a8222ecf5eac4b41..c0c24ca13d883c91904d2ddd9f7a9da420afcf19 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
@@ -59,7 +59,8 @@ Assume {
Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'h':
+[wp] tests/wp_typed/unit_alloc.i:34: Warning:
+ Memory model hypotheses for function 'h':
/*@ behavior 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 9bc96f2981db0f1496e3ae32dd39f01cb210b55c..ff04631dd24c76acef4536e3778263e304db9300 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
@@ -59,7 +59,8 @@ Assume {
Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'h':
+[wp] tests/wp_typed/unit_alloc.i:34: Warning:
+ Memory model hypotheses for function 'h':
/*@ behavior 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 c0eec98834070f47edced3f7b7288673ae2a08bc..1619506b6e983f527754d34c19c907d7547733a8 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
@@ -10,7 +10,8 @@ Goal Post-condition (file tests/wp_typed/unit_ite.i, line 2) in 'check':
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'check':
+[wp] tests/wp_typed/unit_ite.i:3: Warning:
+ Memory model hypotheses for function 'check':
/*@ behavior 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 98b60be4d4acc85fc0c73725a7e1ca124159ed51..55340b288d23736d0d514b6089186eb705bda40d 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
@@ -26,7 +26,8 @@ Goal Assertion 'PJ' (file tests/wp_typed/unit_labels.i, line 10):
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'duplet':
+[wp] tests/wp_typed/unit_labels.i:7: Warning:
+ Memory model hypotheses for function 'duplet':
/*@
behavior typed_ref:
requires \separated(pi, pj, a + (..));
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 9cd81cf810713b1a3524c268452769cbb34bcf1c..0417f4d5c31c88fb7bde5ec3620aecdada871a33 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
@@ -17,7 +17,8 @@ Goal Establishment of Invariant (file tests/wp_typed/unit_loopscope.i, line 13):
Prove: false.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_typed/unit_loopscope.i:9: Warning:
+ Memory model hypotheses for function 'f':
/*@ behavior 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 b49ad5f8dddc52f47a74259da71cc92795e32b34..fe5762e157d97db1da57b23ac857f4d111b3482f 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
@@ -115,7 +115,8 @@ Effect at line 68
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_typed/user_injector.i:58: Warning:
+ Memory model hypotheses for function 'job':
/*@
behavior typed:
requires
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 abbc64b85dacff64fa8d779ed0d10ab167bc9959..b46f36ca8acbd5e1cf5aaf9c0a7198fc31bd59e0 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
@@ -40,7 +40,8 @@ Goal Assigns 'E' in 'swap':
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'swap':
+[wp] tests/wp_typed/user_swap.i:13: Warning:
+ Memory model hypotheses for function 'swap':
/*@
behavior typed_ref:
requires \separated(a, 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 e3baff99bdefb413fbad3518954f3267b4f87eb5..a80625768fac4e994fe0a0474c1a9c49df58afb0 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
@@ -13,7 +13,8 @@
Functions WP Alt-Ergo Total Success
Job - 1 1 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'Write':
+[wp] tests/wp_typed/mvar.i:8: Warning:
+ Memory model hypotheses for function 'Write':
/*@
behavior typed:
requires \separated(p + (..), (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 ab46f16aa40e753281ef5d594fb989f360be4ace..b1b2521268f1a63cbdab716cff1a487867dc4a9c 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
@@ -20,7 +20,8 @@
g 1 - 1 100%
h - 1 1 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'h':
+[wp] tests/wp_typed/unit_alloc.i:34: Warning:
+ Memory model hypotheses for function 'h':
/*@ behavior 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 83a0e03a3acb9543bd411520240ceadc1f72cf4e..8ce55b8c1efb6a863e4adbcb0d84f7db4de7bd27 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
@@ -20,7 +20,8 @@
g 1 - 1 100%
h - 1 1 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'h':
+[wp] tests/wp_typed/unit_alloc.i:34: Warning:
+ Memory model hypotheses for function 'h':
/*@ behavior 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 4417ddd127acc3f894426f6829b8d8b4766afaf2..6a7a2b81e80674e022db315eaea11a9284b6ca84 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
@@ -14,7 +14,8 @@
Functions WP Alt-Ergo Total Success
f 1 - 2 50.0%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_typed/unit_loopscope.i:9: Warning:
+ Memory model hypotheses for function 'f':
/*@ behavior 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 20fdb332cff1128c6e165033300ad73bfea348fc..3cb90f7aac4b67754514a1b166a8e0617605aa87 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
@@ -29,7 +29,8 @@
Functions WP Alt-Ergo Total Success
job 20 - 20 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_typed/user_injector.i:58: Warning:
+ Memory model hypotheses for function 'job':
/*@
behavior typed:
requires
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 93b4fb88899dc8766046ac491738f5ce0f679df6..aff929f01af2b43c36b66626dd8e5ca12a4d9576 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
@@ -25,7 +25,8 @@
Functions WP Alt-Ergo Total Success
job 16 - 16 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_typed/user_injector.i:58: Warning:
+ Memory model hypotheses for function 'job':
/*@
behavior typed_ref:
requires
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 1a4f9fd916dc87ddda1ca6877dad7c9460da89d1..299ef52752ed8594616607474aaddef4bc35ebe1 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
@@ -16,7 +16,8 @@
swap 3 - 3 100%
main 3 - 3 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'swap':
+[wp] tests/wp_typed/user_swap.i:13: Warning:
+ Memory model hypotheses for function 'swap':
/*@
behavior typed_ref:
requires \separated(a, 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 b4a9f732ab57d81a13ed8b594f0a2c991ce7980e..ebe14ffdae03bdf28c428c6be9c0580c661ce305 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
@@ -68,7 +68,8 @@ Assume {
Prove: P_OBS(x_2, x_3, x_4).
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'implicit':
+[wp] tests/wp_usage/caveat.i:17: Warning:
+ Memory model hypotheses for function 'implicit':
/*@
behavior typed_caveat:
requires \separated(a, r);
@@ -76,7 +77,8 @@ Prove: P_OBS(x_2, x_3, x_4).
requires \valid(r);
*/
void implicit(struct S *a, int *r);
-[wp] Warning: Memory model hypotheses for function 'explicit':
+[wp] tests/wp_usage/caveat.i:32: Warning:
+ Memory model hypotheses for function 'explicit':
/*@
behavior typed_caveat:
requires \separated(a, r);
@@ -84,7 +86,8 @@ Prove: P_OBS(x_2, x_3, x_4).
requires \valid(r);
*/
void explicit(struct S *a, int *r);
-[wp] Warning: Memory model hypotheses for function 'observer':
+[wp] tests/wp_usage/caveat.i:47: Warning:
+ Memory model hypotheses for function 'observer':
/*@
behavior typed_caveat:
requires \separated(a, 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 c4439057d741e22283cc74f24ba42ade076657f5..736fa74fbf85b4147c873da56bd003271cd63730 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -97,7 +97,8 @@ Effect at line 25
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_usage/caveat2.i:17: Warning:
+ Memory model hypotheses for function 'job':
/*@
behavior typed_caveat:
requires \separated(p, b + (..));
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 d15c7f73b49722c9b671268208fb84518250c69e..b0856e556ee84230cff8be109455255cf158f986 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
@@ -154,7 +154,8 @@ Effect at line 24
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
+[wp] tests/wp_usage/caveat_range.i:16: Warning:
+ Memory model hypotheses for function 'reset':
/*@ behavior typed_caveat:
requires \valid(p + (..)); */
void reset(struct S *p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
index 9d693417c6b4613aa23c294ebdad6bdbea6a18e8..a4c1a22338abda8b5e27223b7742299ccddeeb1f 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
@@ -43,7 +43,8 @@ Function cup:
[wp] [CFG] Goal by_reference_in_code_annotation_no_exit_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] No proof obligations
-[wp] Warning: Memory model hypotheses for function 'by_value_in_code_annotation':
+[wp] tests/wp_usage/code_spec.i:56: Warning:
+ Memory model hypotheses for function 'by_value_in_code_annotation':
/*@
behavior typed:
requires
@@ -53,7 +54,8 @@ Function cup:
);
*/
void by_value_in_code_annotation(int v, int *p, int *q);
-[wp] Warning: Memory model hypotheses for function 'by_reference_in_code_annotation':
+[wp] tests/wp_usage/code_spec.i:71: Warning:
+ Memory model hypotheses for function 'by_reference_in_code_annotation':
/*@ behavior typed:
requires \separated(p, &p1, &p2, &p3, &p4, &p5, &p6); */
void by_reference_in_code_annotation(int *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 0243fc9b1786ecd5d354be89f6212db6e707dc29..76498068b73e8313c3096f7621c291b9d72f8f79 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
@@ -19,7 +19,8 @@ Goal Instance of 'Pre-condition (file tests/wp_usage/global.c, line 14) in 'foo'
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'foo':
+[wp] tests/wp_usage/global.c:16: Warning:
+ Memory model hypotheses for function 'foo':
/*@ behavior 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 6d03c92ee56c2b284a167e6eb2a17091cf840e08..221fdfb3bc9174910217852b81d8f96d1b19a713 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
@@ -19,7 +19,8 @@ Goal Instance of 'Pre-condition (file tests/wp_usage/global.c, line 14) in 'foo'
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'foo':
+[wp] tests/wp_usage/global.c:16: Warning:
+ Memory model hypotheses for function 'foo':
/*@ behavior typed_ref:
requires \separated(a, &GLOBAL);
requires \valid(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 71a2cdaccb60d2b018b7d2eaa18b5ce4cbc57b8c..7d5d683720a246b549814285dd7d10c06b54d586 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
@@ -167,7 +167,8 @@ Effect at line 59
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'memcpy_context_vars':
+[wp] tests/wp_usage/issue-189-bis.i:48: Warning:
+ Memory model hypotheses for function 'memcpy_context_vars':
/*@
behavior typed:
requires \separated(src, dst);
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 0b9c5b7d7e604f10f869d9801c20aba6bed6f7ea..cfc85d0a9b785451261c72d100337868dc307269 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
@@ -22,7 +22,8 @@ Effect at line 17
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_usage/issue-189.i:16: Warning:
+ Memory model hypotheses for function 'f':
/*@
behavior typed_caveat:
requires \separated(ptr, src);
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 11cce5896b425f90d83d3c0d611d121931e71eb0..e0ce794b3c57c0720ecf99a465a0af19e580c703 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
@@ -17,7 +17,8 @@ Goal Pre-condition (file tests/wp_usage/ref-usage-lemmas.i, line 30) in 'main':
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'foo':
+[wp] tests/wp_usage/ref-usage-lemmas.i:26: Warning:
+ Memory model hypotheses for function 'foo':
/*@ behavior 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 6c1a2b8821961dcbaf564314c55b39872a1ef6bc..dca6dab77af85b269ae738a7b0560be789294e31 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
@@ -20,7 +20,8 @@
Functions WP Alt-Ergo Total Success
job 6 3 9 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_usage/caveat2.i:17: Warning:
+ Memory model hypotheses for function 'job':
/*@
behavior typed_caveat:
requires \separated(p, b + (..));
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 050004166a73ac6f66a23eadb0131b5b510a598c..c931af606d284c8aa5c2109b80eebc701a9004c9 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
@@ -22,7 +22,8 @@
Functions WP Alt-Ergo Total Success
reset 7 5 12 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
+[wp] tests/wp_usage/caveat_range.i:16: Warning:
+ Memory model hypotheses for function 'reset':
/*@ behavior 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 c2679dccf0ddd1ca3dbebec9e4eb51a652063629..d0d733d8c658a55cfeafcbee29b99655a3a0471f 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
@@ -20,7 +20,8 @@
Functions WP Alt-Ergo Total Success
memcpy_context_vars 7 3 10 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'memcpy_context_vars':
+[wp] tests/wp_usage/issue-189-bis.i:48: Warning:
+ Memory model hypotheses for function 'memcpy_context_vars':
/*@
behavior typed:
requires \separated(src, dst);