From 4dcfa5f1aff8df5566cc30dbb2f4537b8572b130 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 6 Oct 2020 16:22:59 +0200
Subject: [PATCH] [wp] Localize memory hypotheses warnings
---
src/plugins/wp/MemoryContext.ml | 2 +-
.../wp_acsl/oracle/assigns_path.res.oracle | 3 ++-
.../wp_acsl/oracle/chunk_typing.res.oracle | 3 ++-
.../tests/wp_acsl/oracle/pointer.res.oracle | 6 +++--
.../oracle_qualif/assigns_path.res.oracle | 3 ++-
.../oracle_qualif/chunk_typing.res.oracle | 3 ++-
.../oracle_qualif/pointer.0.res.oracle | 3 ++-
.../oracle_qualif/pointer.1.res.oracle | 3 ++-
.../wp/tests/wp_bts/oracle/bts0843.res.oracle | 3 ++-
.../tests/wp_bts/oracle/bts_1828.0.res.oracle | 3 ++-
.../tests/wp_bts/oracle/bts_1828.1.res.oracle | 3 ++-
.../wp_bts/oracle_qualif/bts0843.res.oracle | 3 ++-
.../oracle_qualif/bts_1828.0.res.oracle | 3 ++-
.../oracle_qualif/bts_1828.1.res.oracle | 3 ++-
.../oracle/frama_c_exo3_solved.old.res.oracle | 3 ++-
.../frama_c_exo3_solved.old.v2.res.oracle | 3 ++-
.../frama_c_exo3_solved.old.res.oracle | 3 ++-
.../frama_c_exo3_solved.old.v2.res.oracle | 3 ++-
.../alias_assigns_hypotheses.0.res.oracle | 27 ++++++++++++-------
.../tests/wp_hoare/oracle/byref.1.res.oracle | 9 ++++---
.../wp_hoare/oracle/dispatch_var.res.oracle | 18 ++++++++-----
.../oracle/dispatch_var2.0.res.oracle | 12 ++++++---
.../oracle/dispatch_var2.1.res.oracle | 12 ++++++---
.../wp_hoare/oracle/reference.res.oracle | 15 +++++++----
.../oracle/reference_and_struct.res.oracle | 9 ++++---
.../oracle/reference_array.res.oracle | 12 ++++++---
.../wp_hoare/oracle/refguards.res.oracle | 9 ++++---
.../alias_assigns_hypotheses.res.oracle | 27 ++++++++++++-------
.../wp_hoare/oracle_qualif/byref.1.res.oracle | 9 ++++---
.../oracle_qualif/dispatch_var.res.oracle | 18 ++++++++-----
.../oracle_qualif/dispatch_var2.0.res.oracle | 12 ++++++---
.../oracle_qualif/dispatch_var2.1.res.oracle | 12 ++++++---
.../oracle_qualif/reference.res.oracle | 15 +++++++----
.../reference_and_struct.res.oracle | 9 ++++---
.../oracle_qualif/reference_array.res.oracle | 12 ++++++---
.../oracle_qualif/refguards.res.oracle | 9 ++++---
.../tests/wp_plugin/oracle/dynamic.res.oracle | 12 ++++++---
.../wp_plugin/oracle/overassign.res.oracle | 6 +++--
.../wp_plugin/oracle/post_assigns.res.oracle | 3 ++-
.../wp/tests/wp_plugin/oracle/sep.res.oracle | 21 ++++++++++-----
.../wp_plugin/oracle/subset_fopen.res.oracle | 3 ++-
.../wp_plugin/oracle/volatile.0.res.oracle | 3 ++-
.../wp_plugin/oracle/volatile.1.res.oracle | 3 ++-
.../oracle_qualif/dynamic.res.oracle | 12 ++++++---
.../oracle_qualif/overassign.res.oracle | 6 +++--
.../oracle_qualif/post_assigns.res.oracle | 3 ++-
.../oracle_qualif/subset_fopen.res.oracle | 3 ++-
.../wp_tip/oracle/chunk_printing.res.oracle | 6 +++--
.../tests/wp_typed/oracle/mvar.0.res.oracle | 3 ++-
.../tests/wp_typed/oracle/mvar.1.res.oracle | 3 ++-
.../wp_typed/oracle/unit_alloc.0.res.oracle | 3 ++-
.../wp_typed/oracle/unit_alloc.1.res.oracle | 3 ++-
.../wp_typed/oracle/unit_ite.1.res.oracle | 3 ++-
.../wp_typed/oracle/unit_labels.1.res.oracle | 3 ++-
.../oracle/unit_loopscope.1.res.oracle | 3 ++-
.../wp_typed/oracle/user_injector.res.oracle | 3 ++-
.../wp_typed/oracle/user_swap.1.res.oracle | 3 ++-
.../wp_typed/oracle_qualif/mvar.res.oracle | 3 ++-
.../oracle_qualif/unit_alloc.0.res.oracle | 3 ++-
.../oracle_qualif/unit_alloc.1.res.oracle | 3 ++-
.../oracle_qualif/unit_loopscope.1.res.oracle | 3 ++-
.../oracle_qualif/user_injector.0.res.oracle | 3 ++-
.../oracle_qualif/user_injector.1.res.oracle | 3 ++-
.../oracle_qualif/user_swap.1.res.oracle | 3 ++-
.../tests/wp_usage/oracle/caveat.1.res.oracle | 9 ++++---
.../tests/wp_usage/oracle/caveat2.res.oracle | 3 ++-
.../wp_usage/oracle/caveat_range.res.oracle | 3 ++-
.../wp_usage/oracle/code_spec.res.oracle | 6 +++--
.../tests/wp_usage/oracle/global.1.res.oracle | 3 ++-
.../tests/wp_usage/oracle/global.2.res.oracle | 3 ++-
.../oracle/issue-189-bis.1.res.oracle | 3 ++-
.../wp_usage/oracle/issue-189.2.res.oracle | 3 ++-
.../oracle/ref-usage-lemmas.res.oracle | 3 ++-
.../wp_usage/oracle_qualif/caveat2.res.oracle | 3 ++-
.../oracle_qualif/caveat_range.res.oracle | 3 ++-
.../oracle_qualif/issue-189-bis.1.res.oracle | 3 ++-
76 files changed, 317 insertions(+), 159 deletions(-)
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 7a295a841fb..b325350326a 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 b8ebbadea5e..85d0655b52c 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 f318abf289f..cb505e19fd9 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 4339266bbaf..193a70bc4bf 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 180d946c317..d05bde7cc84 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 48e98d4fa14..f5f8f9ccd56 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 9e0fd3122c6..5dee9e18dea 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 5e0172dd87d..60898d58685 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 8c6fd6aed1b..65fbcabad5f 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 640c9952226..ebbd70f4cdb 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 5b00c3b48f3..fdf25268ad2 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 fbd210f679c..a522bf115dd 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 91203bd8a7c..9bffe58d0b5 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 e5edde37e9b..c85bac0087b 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 e21f8f5fe4b..d44fe2c4e6c 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 0a5004c6765..68e0c5d7ad6 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 920eb2e7847..70ff1ce19f1 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 86908f16b54..a87e532706d 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 832baab84eb..793f91fafc8 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 54ad8489278..1fa158d4b18 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 a331a124739..3b0db526829 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 61bf6b67367..9920ee4d4ce 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 44ae58e7b74..932c183de67 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 3b23754654d..c7395b1a724 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 fc78cf9e70f..f816e6df044 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 bc9d8f6a5c0..fe649246798 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 59c0568ee15..bb63bebf59a 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 33a25d793ff..99cd98673ce 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 48e1936e195..816e897df18 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 c2c4c3b9683..aa66d23b2fc 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 b5878139820..9172fe5d07b 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 7a50ede52eb..26521bbd90e 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 293e74343d6..f90e23c73a5 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 61dba2feb73..48133b9d6ee 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 67a8d5d5f14..4a84b4eb4b8 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 02a4bffe2c4..9a42e648075 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 e71c6e9ae9a..91365d446b7 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 a3bcc315fda..6f296e1d079 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 45299879b14..d557391b191 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 fdfb80b6c39..61c35549a7f 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 719b55d6491..b43689ed846 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 8f0c8d4ce8a..015937705a8 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 8f7b2282f20..8736e619bd1 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 9144906c8da..f2e983f6020 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 5bfb2cf3e34..48f494c79a7 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 7333f0d562c..bde4fe1a240 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 9ab32fb6c08..14f5f8935de 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 02cc117a476..560e6143624 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 2394b867cc2..21e31a09591 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 5b2b4174280..2c2ed44ef41 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 498ce46ee4c..c0c24ca13d8 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 9bc96f2981d..ff04631dd24 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 c0eec988340..1619506b6e9 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 98b60be4d4a..55340b288d2 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 9cd81cf8107..0417f4d5c31 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 b49ad5f8ddd..fe5762e157d 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 abbc64b85da..b46f36ca8ac 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 e3baff99bde..a80625768fa 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 ab46f16aa40..b1b2521268f 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 83a0e03a3ac..8ce55b8c1ef 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 4417ddd127a..6a7a2b81e80 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 20fdb332cff..3cb90f7aac4 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 93b4fb88899..aff929f01af 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 1a4f9fd916d..299ef52752e 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 b4a9f732ab5..ebe14ffdae0 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 c4439057d74..736fa74fbf8 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 d15c7f73b49..b0856e556ee 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 9d693417c6b..a4c1a22338a 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 0243fc9b178..76498068b73 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 6d03c92ee56..221fdfb3bc9 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 71a2cdaccb6..7d5d683720a 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 0b9c5b7d7e6..cfc85d0a9b7 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 11cce5896b4..e0ce794b3c5 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 6c1a2b88219..dca6dab77af 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 050004166a7..c931af606d2 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 c2679dccf0d..d0d733d8c65 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);
--
GitLab