Commit 4dcfa5f1 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Localize memory hypotheses warnings

parent 0cd93c52
......@@ -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)
......
......@@ -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);
......@@ -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 + (..));
......
......@@ -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);
......@@ -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);
......@@ -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 + (..));
......
......@@ -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);
......@@ -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);
......@@ -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);
......@@ -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);
......@@ -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);
......
......@@ -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);
......@@ -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);
......@@ -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);
......
......@@ -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 + (..));
......
......@@ -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 + (..));
......
......@@ -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 + (..));
......
......@@ -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 + (..));
......
......@@ -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});
......
......@@ -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);
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment