Skip to content
Snippets Groups Projects
Commit d98a39d2 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] re-order separation hypotheses

parent f98f4d68
No related branches found
No related tags found
No related merge requests found
Showing
with 87 additions and 76 deletions
......@@ -210,9 +210,20 @@ let valid_or_null_region loc r =
let null = term ~loc Tnull t.term_type in
por (valid_region loc r, prel ~loc (Req, t, null))
let simplify ps =
List.sort_uniq Logic_utils.compare_predicate
(List.filter (fun p -> not(Logic_utils.is_trivially_true p)) ps)
let rec rank p = match p.pred_content with
| Pvalid _ -> 1
| Pseparated _ -> 2
| Pimplies(_,p) -> rank p
| Por(p,q) | Pand(p,q) -> max (rank p) (rank q)
| _ -> 0
let compare p q =
let r = rank p - rank q in
if r <> 0 then r else Logic_utils.compare_predicate p q
let normalize ps =
List.sort_uniq compare @@
List.filter (fun p -> not(Logic_utils.is_trivially_true p)) ps
let ptrset { term_type = t } =
let open Logic_typing in
......@@ -356,8 +367,8 @@ let clauses_of_partition kf loc p =
let context_valid = List.map (valid_region loc) (context_zones p) in
let nullable_valid = List.map (valid_or_null_region loc) (nullable_zones p) in
let reqs = main_sep @ assigns_sep_req @ context_valid @ nullable_valid in
let reqs = simplify reqs in
let ens = simplify assigns_sep_ens in
let reqs = normalize reqs in
let ens = normalize assigns_sep_ens in
reqs, ens
(* Computes conditions from return *)
......@@ -386,7 +397,7 @@ let out_pointers_separation kf loc p =
let globals = global_zones p in
List.map (fun t -> term_separated_from_regions loc t globals) asgnd_ptrs
in
simplify (formals_separation @ globals_separation)
normalize (formals_separation @ globals_separation)
(* Computes all conditions from behavior *)
let compute_behavior kf name hypotheses_computer =
......
......@@ -48,8 +48,8 @@ Prove: global(L_two_24) != one_0.
Memory model hypotheses for function 'global_frame':
/*@
behavior wp_typed_ref:
requires \separated(zero, one);
requires \valid(one);
requires \valid(zero);
requires \separated(zero, one);
*/
void global_frame(int *one, int arg);
......@@ -21,8 +21,8 @@
Memory model hypotheses for function 'global_frame':
/*@
behavior wp_typed_ref:
requires \separated(zero, one);
requires \valid(one);
requires \valid(zero);
requires \separated(zero, one);
*/
void global_frame(int *one, int arg);
......@@ -56,8 +56,8 @@
Memory model hypotheses for function 'equal_elements':
/*@
behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
requires \separated(v1, v2, a + (..));
*/
void equal_elements(int *a, int *v1, int *v2);
......@@ -57,8 +57,8 @@
Memory model hypotheses for function 'equal_elements':
/*@
behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
requires \separated(v1, v2, a + (..));
*/
void equal_elements(int *a, int *v1, int *v2);
......@@ -48,9 +48,9 @@
Memory model hypotheses for function 'equal_elements':
/*@
behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
requires \separated(v1, v2, a + (..));
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
......
......@@ -49,9 +49,9 @@
Memory model hypotheses for function 'equal_elements':
/*@
behavior wp_typed_ref:
requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
requires \separated(v1, v2, a + (..));
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
......
......@@ -515,10 +515,10 @@ Prove: true.
Memory model hypotheses for function 'ref_ctr_nr':
/*@
behavior wp_typed_ref:
requires \separated(ref, ref1, ref2);
requires \valid(ref);
requires \valid(ref1);
requires \valid(ref2);
requires \separated(ref, ref1, ref2);
*/
int ref_ctr_nr(int *ref, int *ref1, int *ref2);
[wp] tests/wp_hoare/dispatch_var.i:158: Warning:
......
......@@ -142,13 +142,13 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 58) in 'assigns_ptr'' in 'call_assigns_ptr_bad' at call 'assigns_ptr' (file tests/wp_hoare/memory_hypotheses_checking.i, line 70)
:
Prove: false.
Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 58) in 'assigns_ptr'' in 'call_assigns_ptr_bad' at call 'assigns_ptr' (file tests/wp_hoare/memory_hypotheses_checking.i, line 70)
:
Prove: true.
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
......@@ -194,14 +194,14 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_bad' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 53)
:
Prove: false.
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_rw(Malloc_0, global(G_g_20), 1).
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_bad' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 53)
:
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_rw(Malloc_0, global(G_g_20), 1).
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
......@@ -220,14 +220,14 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_ok' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 47)
:
Prove: true.
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_rw(Malloc_0[L_l_46 <- 1], global(L_l_46), 1).
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_ok' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 47)
:
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_rw(Malloc_0[L_l_46 <- 1], global(L_l_46), 1).
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
......@@ -246,13 +246,13 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_sep' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 24)
:
Prove: false.
Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_sep' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 24)
:
Prove: true.
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
......@@ -283,14 +283,14 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_valid' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 34)
:
Prove: true.
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_rw(Malloc_0[L_l_37 <- 0], global(L_l_37), 1).
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_valid' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 34)
:
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_rw(Malloc_0[L_l_37 <- 0], global(L_l_37), 1).
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
......@@ -341,8 +341,8 @@ int g;
/*@ assigns \nothing;
behavior wp_typed_ref:
requires \separated(p_0, &g);
requires \valid(p_0);
requires \separated(p_0, &g);
*/
int sep(int *p_0)
{
......@@ -382,8 +382,8 @@ int *p;
/*@ assigns \nothing;
behavior wp_typed_ref:
requires \separated(p, &g);
requires \valid(p);
requires \separated(p, &g);
*/
int gptr_sep(void)
{
......@@ -414,8 +414,8 @@ void call_gptr_sep_bad(void)
/*@ assigns *p_0;
behavior wp_typed_ref:
requires \separated(p_0, &g);
requires \valid(p_0);
requires \separated(p_0, &g);
*/
void assigns_ptr(int *p_0)
{
......
......@@ -150,9 +150,9 @@ Prove: true.
Memory model hypotheses for function 'f2':
/*@
behavior wp_typed_ref:
requires \separated(p2, q);
requires \valid(p2);
requires \valid(q);
requires \separated(p2, q);
*/
int f2(int *p2, int *q);
[wp] tests/wp_hoare/reference.i:37: Warning:
......
......@@ -72,26 +72,26 @@ Prove: d != c.
Memory model hypotheses for function 'f':
/*@
behavior wp_typed_ref:
requires \separated(c, d, {a + (..), b + (..)});
requires \valid(c);
requires \valid(d);
requires \separated(c, d, {a + (..), b + (..)});
*/
void f(int *a, int *b, int *c, int *d, int k);
[wp] tests/wp_hoare/refguards.i:25: Warning:
Memory model hypotheses for function 'h':
/*@
behavior wp_typed_ref:
requires \separated(c, d);
requires \valid(c);
requires \valid(d);
requires \separated(c, d);
*/
void h(int *c, int *d, int k);
[wp] tests/wp_hoare/refguards.i:39: Warning:
Memory model hypotheses for function 's':
/*@
behavior wp_typed_ref:
requires \separated(c, d);
requires \valid(c);
requires \valid(d);
requires \separated(c, d);
*/
void s(int **c, int **d, int k);
......@@ -118,10 +118,10 @@
Memory model hypotheses for function 'ref_ctr_nr':
/*@
behavior wp_typed_ref:
requires \separated(ref, ref1, ref2);
requires \valid(ref);
requires \valid(ref1);
requires \valid(ref2);
requires \separated(ref, ref1, ref2);
*/
int ref_ctr_nr(int *ref, int *ref1, int *ref2);
[wp] tests/wp_hoare/dispatch_var.i:158: Warning:
......
......@@ -10,23 +10,23 @@
[wp] [Qed] Goal typed_ref_call_sep_ok_call_sep_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_sep_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_sep_assigns_normal : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires : Unsuccess
[wp] [Qed] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires_2 : Unsuccess
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_exit_part1 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_exit_part2 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires : Unsuccess
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_gptr_sep_assigns : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_assigns_normal : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires_2 : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_bad_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_bad_assigns_normal : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires : Unsuccess
[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires_2 : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires_2 : Unsuccess
[wp] [Qed] Goal typed_ref_assigns_ptr_assigns : Valid
[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_assigns_normal : Valid
......@@ -34,8 +34,8 @@
[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_call_assigns_ptr_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_assigns_normal : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires : Unsuccess
[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires : Valid
[wp] [Alt-Ergo] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires_2 : Unsuccess
[wp] [Qed] Goal typed_ref_add_return_ok_ensures : Valid
[wp] [Qed] Goal typed_ref_add_return_ok_assigns : Valid
[wp] [Qed] Goal typed_ref_add_return_ok_wp_typed_ref_ensures : Valid
......
......@@ -45,9 +45,9 @@
Memory model hypotheses for function 'f2':
/*@
behavior wp_typed_ref:
requires \separated(p2, q);
requires \valid(p2);
requires \valid(q);
requires \separated(p2, q);
*/
int f2(int *p2, int *q);
[wp] tests/wp_hoare/reference.i:37: Warning:
......
......@@ -26,26 +26,26 @@
Memory model hypotheses for function 'f':
/*@
behavior wp_typed_ref:
requires \separated(c, d, {a + (..), b + (..)});
requires \valid(c);
requires \valid(d);
requires \separated(c, d, {a + (..), b + (..)});
*/
void f(int *a, int *b, int *c, int *d, int k);
[wp] tests/wp_hoare/refguards.i:25: Warning:
Memory model hypotheses for function 'h':
/*@
behavior wp_typed_ref:
requires \separated(c, d);
requires \valid(c);
requires \valid(d);
requires \separated(c, d);
*/
void h(int *c, int *d, int k);
[wp] tests/wp_hoare/refguards.i:39: Warning:
Memory model hypotheses for function 's':
/*@
behavior wp_typed_ref:
requires \separated(c, d);
requires \valid(c);
requires \valid(d);
requires \separated(c, d);
*/
void s(int **c, int **d, int k);
......@@ -40,11 +40,11 @@ Prove: true.
Memory model hypotheses for function 'nullable_coherence':
/*@
behavior wp_typed_caveat:
requires \valid(g);
requires \valid(p) ∨ p ≡ \null;
requires \separated(g, &x);
requires \separated(p, &x);
requires \valid(g);
requires p ≢ \null ⇒ \separated(g, p, &x);
requires \valid(p) ∨ p ≡ \null;
*/
void nullable_coherence(int *p /*@ wp_nullable */);
[wp] tests/wp_plugin/nullable.i:24: Warning:
......@@ -53,15 +53,15 @@ Prove: true.
behavior wp_typed_caveat:
requires \valid(s);
requires \valid(t);
requires \valid(p) ∨ p ≡ \null;
requires \valid(q) ∨ q ≡ \null;
requires \valid(r) ∨ r ≡ \null;
requires p ≢ \null ⇒ \separated(p, s, t);
requires q ≢ \null ⇒ \separated(q, s, t);
requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
requires r ≢ \null ⇒ \separated(r, s, t);
requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
requires \valid(p) ∨ p ≡ \null;
requires \valid(q) ∨ q ≡ \null;
requires \valid(r) ∨ r ≡ \null;
*/
void nullable_in_context(int *p /*@ wp_nullable */,
int *q /*@ wp_nullable */,
......
......@@ -40,11 +40,11 @@ Prove: true.
Memory model hypotheses for function 'nullable_coherence':
/*@
behavior wp_typed_caveat:
requires \valid(g);
requires \valid(p) ∨ p ≡ \null;
requires \separated(g, &x);
requires \separated(p, &x);
requires \valid(g);
requires p ≢ \null ⇒ \separated(g, p, &x);
requires \valid(p) ∨ p ≡ \null;
*/
void nullable_coherence(int *p /*@ wp_nullable */);
[wp] tests/wp_plugin/nullable_ext.i:28: Warning:
......@@ -53,15 +53,15 @@ Prove: true.
behavior wp_typed_caveat:
requires \valid(s);
requires \valid(t);
requires \valid(p) ∨ p ≡ \null;
requires \valid(q) ∨ q ≡ \null;
requires \valid(r) ∨ r ≡ \null;
requires p ≢ \null ⇒ \separated(p, s, t);
requires q ≢ \null ⇒ \separated(q, s, t);
requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
requires r ≢ \null ⇒ \separated(r, s, t);
requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
requires \valid(p) ∨ p ≡ \null;
requires \valid(q) ∨ q ≡ \null;
requires \valid(r) ∨ r ≡ \null;
*/
void nullable_in_context(int *p /*@ wp_nullable */,
int *q /*@ wp_nullable */,
......
......@@ -69,58 +69,58 @@ Prove: true.
[wp] tests/wp_plugin/sep.i:18: Warning:
Memory model hypotheses for function 'f2_p_a':
/*@ behavior wp_typed_caveat:
requires \separated(p, &a);
requires \valid(p); */
requires \valid(p);
requires \separated(p, &a); */
void f2_p_a(int *p);
[wp] tests/wp_plugin/sep.i:22: Warning:
Memory model hypotheses for function 'f3_p_ab':
/*@
behavior wp_typed_caveat:
requires \separated(p, &a, &b);
requires \valid(p);
requires \separated(p, &a, &b);
*/
void f3_p_ab(int *p);
[wp] tests/wp_plugin/sep.i:26: Warning:
Memory model hypotheses for function 'f4_pq_ab':
/*@
behavior wp_typed_caveat:
requires \separated(p, q, &a, &b);
requires \valid(p);
requires \valid(q);
requires \separated(p, q, &a, &b);
*/
void f4_pq_ab(int *p, int *q);
[wp] tests/wp_plugin/sep.i:30: Warning:
Memory model hypotheses for function 'f5_pq':
/*@
behavior wp_typed_caveat:
requires \separated(p, q);
requires \valid(p);
requires \valid(q);
requires \separated(p, q);
*/
void f5_pq(int *p, int *q);
[wp] tests/wp_plugin/sep.i:34: Warning:
Memory model hypotheses for function 'f6_Pa':
/*@
behavior wp_typed_caveat:
requires \separated(p + (..), &a);
requires \valid(p + (..));
requires \separated(p + (..), &a);
*/
void f6_Pa(int *p, int k);
[wp] tests/wp_plugin/sep.i:43: Warning:
Memory model hypotheses for function 'f7_pq_ad':
/*@
behavior wp_typed_caveat:
requires \separated(p, q, &a, &d);
requires \valid(p);
requires \valid(q);
requires \separated(p, q, &a, &d);
*/
void f7_pq_ad(int *p, int *q);
[wp] tests/wp_plugin/sep.i:49: Warning:
Memory model hypotheses for function 'f8_pq_a':
/*@
behavior wp_typed_caveat:
requires \separated(p, q, &a);
requires \valid(p);
requires \valid(q);
requires \separated(p, q, &a);
*/
void f8_pq_a(int *p, int *q);
......@@ -21,11 +21,11 @@
Memory model hypotheses for function 'nullable_coherence':
/*@
behavior wp_typed_caveat:
requires \valid(g);
requires \valid(p) ∨ p ≡ \null;
requires \separated(g, &x);
requires \separated(p, &x);
requires \valid(g);
requires p ≢ \null ⇒ \separated(g, p, &x);
requires \valid(p) ∨ p ≡ \null;
*/
void nullable_coherence(int *p /*@ wp_nullable */);
[wp] tests/wp_plugin/nullable.i:24: Warning:
......@@ -34,15 +34,15 @@
behavior wp_typed_caveat:
requires \valid(s);
requires \valid(t);
requires \valid(p) ∨ p ≡ \null;
requires \valid(q) ∨ q ≡ \null;
requires \valid(r) ∨ r ≡ \null;
requires p ≢ \null ⇒ \separated(p, s, t);
requires q ≢ \null ⇒ \separated(q, s, t);
requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
requires r ≢ \null ⇒ \separated(r, s, t);
requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
requires \valid(p) ∨ p ≡ \null;
requires \valid(q) ∨ q ≡ \null;
requires \valid(r) ∨ r ≡ \null;
*/
void nullable_in_context(int *p /*@ wp_nullable */,
int *q /*@ wp_nullable */,
......
......@@ -21,11 +21,11 @@
Memory model hypotheses for function 'nullable_coherence':
/*@
behavior wp_typed_caveat:
requires \valid(g);
requires \valid(p) ∨ p ≡ \null;
requires \separated(g, &x);
requires \separated(p, &x);
requires \valid(g);
requires p ≢ \null ⇒ \separated(g, p, &x);
requires \valid(p) ∨ p ≡ \null;
*/
void nullable_coherence(int *p /*@ wp_nullable */);
[wp] tests/wp_plugin/nullable_ext.i:28: Warning:
......@@ -34,15 +34,15 @@
behavior wp_typed_caveat:
requires \valid(s);
requires \valid(t);
requires \valid(p) ∨ p ≡ \null;
requires \valid(q) ∨ q ≡ \null;
requires \valid(r) ∨ r ≡ \null;
requires p ≢ \null ⇒ \separated(p, s, t);
requires q ≢ \null ⇒ \separated(q, s, t);
requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
requires r ≢ \null ⇒ \separated(r, s, t);
requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
requires \valid(p) ∨ p ≡ \null;
requires \valid(q) ∨ q ≡ \null;
requires \valid(r) ∨ r ≡ \null;
*/
void nullable_in_context(int *p /*@ wp_nullable */,
int *q /*@ wp_nullable */,
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment