Commit aae47aab authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] More robust hypotheses behaviors

parent df31b577
......@@ -357,7 +357,7 @@ let compute_behavior kf name hypotheses_computer =
| [], [] -> None
| reqs, ens ->
Some {
b_name = name ;
b_name = Annotations.fresh_behavior_name kf ("wp_" ^ name) ;
b_requires = reqs ;
b_assumes = [] ;
b_post_cond = ens ;
......
......@@ -99,6 +99,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_acsl/assigns_path.i:12: Warning:
Memory model hypotheses for function 'job':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(b + (..), &p); */
void job(int n, int *b);
......@@ -1879,7 +1879,7 @@ Prove: true.
[wp] tests/wp_acsl/chunk_typing.i:21: Warning:
Memory model hypotheses for function 'function':
/*@
behavior typed:
behavior wp_typed:
requires \separated(i16 + (..), (char const *)x + (..));
requires \separated(i32 + (..), (char const *)x + (..));
requires \separated(i64 + (..), (char const *)x + (..));
......
......@@ -142,16 +142,16 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_acsl/funvar_inv.i:26: Warning:
Memory model hypotheses for function 'f':
/*@ behavior hoare:
/*@ behavior wp_hoare:
ensures \separated(\result, (int *)G + (..)); */
int *f(void);
[wp] tests/wp_acsl/funvar_inv.i:40: Warning:
Memory model hypotheses for function 'f2':
/*@ behavior hoare:
/*@ behavior wp_hoare:
ensures \separated(\result, (int *)G + (..)); */
int *f2(void);
[wp] tests/wp_acsl/funvar_inv.i:55: Warning:
Memory model hypotheses for function 'g':
/*@ behavior hoare:
/*@ behavior wp_hoare:
ensures \separated(\result, (int *)G + (..)); */
int *g(void);
......@@ -236,11 +236,11 @@ Prove: false.
------------------------------------------------------------
[wp] tests/wp_acsl/pointer.i:63: Warning:
Memory model hypotheses for function 'compare':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(q + (..), &p); */
void compare(int *q);
[wp] tests/wp_acsl/pointer.i:73: Warning:
Memory model hypotheses for function 'absurd':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(q + (..), &p); */
void absurd(int *q);
......@@ -21,6 +21,6 @@
------------------------------------------------------------
[wp] tests/wp_acsl/assigns_path.i:12: Warning:
Memory model hypotheses for function 'job':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(b + (..), &p); */
void job(int n, int *b);
......@@ -52,7 +52,7 @@
[wp] tests/wp_acsl/chunk_typing.i:21: Warning:
Memory model hypotheses for function 'function':
/*@
behavior typed:
behavior wp_typed:
requires \separated(i16 + (..), (char const *)x + (..));
requires \separated(i32 + (..), (char const *)x + (..));
requires \separated(i64 + (..), (char const *)x + (..));
......
......@@ -28,6 +28,6 @@
------------------------------------------------------------
[wp] tests/wp_acsl/pointer.i:73: Warning:
Memory model hypotheses for function 'absurd':
/*@ behavior typed_ref:
/*@ behavior wp_typed_ref:
requires \separated(q + (..), &p); */
void absurd(int *q);
......@@ -28,6 +28,6 @@
------------------------------------------------------------
[wp] tests/wp_acsl/pointer.i:73: Warning:
Memory model hypotheses for function 'absurd':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(q + (..), &p); */
void absurd(int *q);
......@@ -54,6 +54,6 @@ Prove: true.
------------------------------------------------------------
[wp] tests/wp_bts/bts0843.i:13: Warning:
Memory model hypotheses for function 'f3':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(&p, &p->a); */
void f3(void);
......@@ -67,6 +67,6 @@ Prove: global(L_two_24) != one_0.
------------------------------------------------------------
[wp] tests/wp_bts/bts_1828.i:56: Warning:
Memory model hypotheses for function 'global_frame':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(one, &zero); */
void global_frame(int *one, int arg);
......@@ -47,7 +47,7 @@ Prove: global(L_two_24) != one_0.
[wp] tests/wp_bts/bts_1828.i:56: Warning:
Memory model hypotheses for function 'global_frame':
/*@
behavior typed_ref:
behavior wp_typed_ref:
requires \separated(zero, one);
requires \valid(one);
requires \valid(zero);
......
......@@ -17,6 +17,6 @@
------------------------------------------------------------
[wp] tests/wp_bts/bts0843.i:13: Warning:
Memory model hypotheses for function 'f3':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(&p, &p->a); */
void f3(void);
......@@ -19,6 +19,6 @@
------------------------------------------------------------
[wp] tests/wp_bts/bts_1828.i:56: Warning:
Memory model hypotheses for function 'global_frame':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(one, &zero); */
void global_frame(int *one, int arg);
......@@ -20,7 +20,7 @@
[wp] tests/wp_bts/bts_1828.i:56: Warning:
Memory model hypotheses for function 'global_frame':
/*@
behavior typed_ref:
behavior wp_typed_ref:
requires \separated(zero, one);
requires \valid(one);
requires \valid(zero);
......
......@@ -55,7 +55,7 @@
[wp] tests/wp_gallery/frama_c_exo3_solved.old.c:73: Warning:
Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
......
......@@ -56,7 +56,7 @@
[wp] tests/wp_gallery/frama_c_exo3_solved.old.v2.c:56: Warning:
Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
......
......@@ -47,7 +47,7 @@
[wp] tests/wp_gallery/frama_c_exo3_solved.old.c:73: Warning:
Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
......
......@@ -48,7 +48,7 @@
[wp] tests/wp_gallery/frama_c_exo3_solved.old.v2.c:56: Warning:
Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
......
......@@ -196,24 +196,24 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:17: Warning:
Memory model hypotheses for function 'global_alias':
/*@
behavior typed:
behavior wp_typed:
requires \separated(g_alias, (int *)global + (..), &g_alias);
*/
void global_alias(void);
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:24: Warning:
Memory model hypotheses for function 'global_no_alias':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(g_alias, &g_alias); */
void global_no_alias(void);
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:32: Warning:
Memory model hypotheses for function 'formal_alias':
/*@ behavior typed:
/*@ behavior wp_typed:
requires \separated(f_alias, (int *)global + (..)); */
void formal_alias(int *f_alias);
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:48: Warning:
Memory model hypotheses for function 'formal_alias_array':
/*@
behavior typed:
behavior wp_typed:
requires \separated((int *)global + (..), &(*alias_array)[0 .. 1]);
requires \separated(alias_array + (..), (int *)global + (..));
*/
......@@ -221,7 +221,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:61: Warning:
Memory model hypotheses for function 'field_alias':
/*@
behavior typed:
behavior wp_typed:
requires \separated((int *)global + (..), &x->x);
requires \separated(x, (int *)global + (..));
*/
......@@ -229,7 +229,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:73: Warning:
Memory model hypotheses for function 'field_range_alias':
/*@
behavior typed:
behavior wp_typed:
requires \separated((int *)global + (..), &(x + (0 .. 3))->x);
requires \separated(x + (..), (int *)global + (..));
*/
......@@ -237,7 +237,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:81: Warning:
Memory model hypotheses for function 'set_alias':
/*@
behavior typed:
behavior wp_typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
*/
......@@ -245,7 +245,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:92: Warning:
Memory model hypotheses for function 'comprehension_alias':
/*@
behavior typed:
behavior wp_typed:
requires
\separated(
(int *)global + (..), &g_alias,
......@@ -256,7 +256,7 @@ Prove: true.
[wp] tests/wp_hoare/alias_assigns_hypotheses.i:102: Warning:
Memory model hypotheses for function 'union_alias':
/*@
behavior typed:
behavior wp_typed:
requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
requires \separated(f_alias, (int *)global + (..), &g_alias);
*/
......
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