diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 0a8086800c9cb6e6c9e661f3cc8be35b0346d2a0..1b1066105cb0354d9d327f72617a2a2d9b911fbf 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -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 =
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 1f183b1d30a1530c5c404f9a38f7ed12fec5d9ff..9c383998a35a6db6956fd0e37c775bc07059fa59 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
@@ -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);
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 43305903b452ccabf5e96e46b022d2bfe3c1ffce..e9a2a01d9a210f37acaaa53be63d723f7baf2541 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
@@ -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);
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 56bb306558b56d74141556fc1b026d735ef9cfe9..5508bc1831913be6943b2cc4f680f7b4d23fcbd7 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
@@ -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);
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 53078f53cb88bbc0681c1ce463aef6b08bf1de0e..87430ad4b3c1a897ffe57842d2ad079a105b7649 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
@@ -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);
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 3903ba3a3a32a691f6e6e2bce73a83b71362f378..174cfa7521504fd213dc75ca4404ea89dddb4faa 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
@@ -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...
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 1dfeafb91d559189ced438c76169d59f9f36c303..cfbc31146758fcdad382bd59ca15be2c53d18327 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
@@ -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...
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 03056370c4a6760b6e4e1e2f3662a4c7bf5753a0..30d6f05c1f7c75c51330593d503e43a92237da15 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
@@ -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:
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle
index 380a7e0cc8ace27dc70721782cf090990ab2631b..142b8eba2461dd41529943de1b117ebcb619649d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle
@@ -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)
{
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 bf4453996e1f0c3f7c0390b232a6c5e86e4608d0..3d3946ce97f51a2657303d810fb22191ebf65aec 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
@@ -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:
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 b99e101310280266d0fc3cf756af8bf32fabd5d8..535d8556ba56a0e495dfbb31d6796d3bee7b3636 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
@@ -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);
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 ab588be9a5c14dfaecd979bc01834341e6c05cef..66bc5879f093902b5614de36af3cbf81025e4f34 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
@@ -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:
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle
index 6a5957ad9bc912905cd60d35a230bb32192e39ea..da1d58667029622f44e24d74f24031b12720acb4 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle
@@ -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
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 6fa2c547d939685057c4e3ce840a76ab810eb7e8..c94049ea06d84693c16c54c4dc50a3e5083ea89c 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
@@ -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:
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 3fba6a750b4f8d97faebe8f14aca0aa61237fea0..549d47287ee22c85592ea76b95d7b7032aca6afa 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
@@ -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);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
index 541dd3c634a862bbb35c5d11ff0f42c17ad77cfb..1fe84b7fa72fb41c754482abcee25af6e247c822 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
@@ -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 */,
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle
index 828cc1502c5d19497103bd8850cdbf29ff0f6cbc..b4246e6986ee28aa5501e570f37ff31edc9d1282 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle
@@ -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 */,
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 e5d8aa84c061c2c39a06fe1f5257ffadeaea8003..24c245a193b32ecbb0357aa353d2e21d9bce3995 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
@@ -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);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
index 225a0af153d83e49ae82063233720bcf48133f6f..a63862b2bf46f677cdb87a010e4272ceff395884 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
@@ -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 */,
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
index 187f1b109f20d58c6844ef352644d40ca2e64d19..1f2fed4938befc5db60a585320ff3e63bce02d74 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
@@ -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 */,
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 7a7b1b25d56460d9600a2462fbc1f0b38cc49dd2..24ac613e94a8d5f7e266beeee05e591a8c77d78e 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
@@ -30,8 +30,8 @@ Prove: true.
Memory model hypotheses for function 'duplet':
/*@
behavior wp_typed_ref:
- requires \separated(pi, pj, a + (..));
requires \valid(pi);
requires \valid(pj);
+ requires \separated(pi, pj, a + (..));
*/
void duplet(int *a, int *pi, int *pj);
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 e571b4fc2cce83e61a9d3f99da28c56e0219ce79..26c949f5c0cd9122a79829c5f595a18b0ad69a14 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
@@ -44,8 +44,8 @@ Prove: true.
Memory model hypotheses for function 'swap':
/*@
behavior wp_typed_ref:
- requires \separated(a, b);
requires \valid(a);
requires \valid(b);
+ requires \separated(a, b);
*/
void swap(int *a, int *b);
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 ad44942e79c58b466fce26436dad805a9512eab4..5d5ce1185b2e1c7d41d297886f473249cfc9c7df 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
@@ -29,11 +29,11 @@
Memory model hypotheses for function 'job':
/*@
behavior wp_typed_ref:
+ requires \valid(error);
requires
\separated(
error, (int *)service_id + (..), (int *)service_result + (..), &seq,
&service_cpt
);
- requires \valid(error);
*/
int job(int a, int b, int *error);
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 d37ff58f250004ef4d1fb0e0262f230040f9f336..18eff921deab26414b4b24426d59fa1a2bb7d5e1 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
@@ -20,8 +20,8 @@
Memory model hypotheses for function 'swap':
/*@
behavior wp_typed_ref:
- requires \separated(a, b);
requires \valid(a);
requires \valid(b);
+ requires \separated(a, b);
*/
void swap(int *a, int *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 7f6f4e1316280036e5df8c8d578bbb2b5e487f1b..0141c03ea9ff5368e80b619ad7ce64c3253d72c0 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
@@ -72,26 +72,26 @@ Prove: P_OBS(x_2, x_3, x_4).
Memory model hypotheses for function 'implicit':
/*@
behavior wp_typed_caveat:
- requires \separated(a, r);
requires \valid(a);
requires \valid(r);
+ requires \separated(a, r);
*/
void implicit(struct S *a, int *r);
[wp] tests/wp_usage/caveat.i:32: Warning:
Memory model hypotheses for function 'explicit':
/*@
behavior wp_typed_caveat:
- requires \separated(a, r);
requires \valid(a);
requires \valid(r);
+ requires \separated(a, r);
*/
void explicit(struct S *a, int *r);
[wp] tests/wp_usage/caveat.i:47: Warning:
Memory model hypotheses for function 'observer':
/*@
behavior wp_typed_caveat:
- requires \separated(a, r);
requires \valid(a);
requires \valid(r);
+ requires \separated(a, r);
*/
void observer(struct S *a, int *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 bd126749ac28da329e21c30afd6113528bb91909..7ec4d49d41a9cc9cf35cc6aa9ab3dd2c08c11c9d 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -101,8 +101,8 @@ Prove: true.
Memory model hypotheses for function 'job':
/*@
behavior wp_typed_caveat:
- requires \separated(p, b + (..));
requires \valid(b + (..));
requires \valid(p);
+ requires \separated(p, b + (..));
*/
void job(struct S *p, int n, int *b);
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 3489aa287459e7a28ac2466a765b8a28f44a3e89..7bb8969a653815ed38f4c1d7a8033b3de5e92220 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
@@ -23,7 +23,7 @@ Prove: true.
Memory model hypotheses for function 'foo':
/*@
behavior wp_typed_ref:
- requires \separated(a, &GLOBAL);
requires \valid(a);
+ requires \separated(a, &GLOBAL);
*/
void foo(int *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 c15cbee10c3bd49b6bdb5e70c103a1ebac5cb9ff..0fb3ea0ed2e6643f287e6cedf372596e6086c6f1 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
@@ -171,8 +171,8 @@ Prove: true.
Memory model hypotheses for function 'memcpy_context_vars':
/*@
behavior wp_typed:
- requires \separated(src, dst);
requires \valid(dst);
requires \valid(src);
+ requires \separated(src, dst);
*/
void memcpy_context_vars(unsigned char *src, unsigned char *dst, int len);
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 5cd9f57c585ba881735715218f8d80be0aab2e2d..0114ddb64681e6f4636f2d82a07fdb25b9f291b4 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
@@ -26,7 +26,7 @@ Prove: true.
Memory model hypotheses for function 'f':
/*@
behavior wp_typed_caveat:
- requires \separated(ptr, src);
requires \valid(ptr);
+ requires \separated(ptr, src);
*/
void f(char *ptr, char const *src, unsigned int idx);
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 86f77567c02d0caf7aab6020ddf1b5cb07631098..5ebef0000b8e36cb669571dd841f5ee001c4a791 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
@@ -24,8 +24,8 @@
Memory model hypotheses for function 'job':
/*@
behavior wp_typed_caveat:
- requires \separated(p, b + (..));
requires \valid(b + (..));
requires \valid(p);
+ requires \separated(p, b + (..));
*/
void job(struct S *p, int n, int *b);
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 e73a38c074fdf04dbda90f7e6ef41eaca850a587..4a5c45145f618785311b2456d1172e1cdfc203e2 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
@@ -24,8 +24,8 @@
Memory model hypotheses for function 'memcpy_context_vars':
/*@
behavior wp_typed:
- requires \separated(src, dst);
requires \valid(dst);
requires \valid(src);
+ requires \separated(src, dst);
*/
void memcpy_context_vars(unsigned char *src, unsigned char *dst, int len);