From d98a39d276cd48ae73574a20f56cadfd76fbd7c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 26 Feb 2021 16:25:03 +0100
Subject: [PATCH] [wp] re-order separation hypotheses
---
src/plugins/wp/MemoryContext.ml | 23 +++++++++----
.../tests/wp_bts/oracle/bts_1828.1.res.oracle | 2 +-
.../oracle_qualif/bts_1828.1.res.oracle | 2 +-
.../oracle/frama_c_exo3_solved.old.res.oracle | 2 +-
.../frama_c_exo3_solved.old.v2.res.oracle | 2 +-
.../frama_c_exo3_solved.old.res.oracle | 2 +-
.../frama_c_exo3_solved.old.v2.res.oracle | 2 +-
.../wp_hoare/oracle/dispatch_var.res.oracle | 2 +-
.../memory_hypotheses_checking.res.oracle | 32 +++++++++----------
.../wp_hoare/oracle/reference.res.oracle | 2 +-
.../wp_hoare/oracle/refguards.res.oracle | 6 ++--
.../oracle_qualif/dispatch_var.res.oracle | 2 +-
.../memory_hypotheses_checking.res.oracle | 20 ++++++------
.../oracle_qualif/reference.res.oracle | 2 +-
.../oracle_qualif/refguards.res.oracle | 6 ++--
.../wp_plugin/oracle/nullable.res.oracle | 10 +++---
.../wp_plugin/oracle/nullable_ext.res.oracle | 10 +++---
.../wp/tests/wp_plugin/oracle/sep.res.oracle | 16 +++++-----
.../oracle_qualif/nullable.res.oracle | 10 +++---
.../oracle_qualif/nullable_ext.res.oracle | 10 +++---
.../wp_typed/oracle/unit_labels.1.res.oracle | 2 +-
.../wp_typed/oracle/user_swap.1.res.oracle | 2 +-
.../oracle_qualif/user_injector.1.res.oracle | 2 +-
.../oracle_qualif/user_swap.1.res.oracle | 2 +-
.../tests/wp_usage/oracle/caveat.1.res.oracle | 6 ++--
.../tests/wp_usage/oracle/caveat2.res.oracle | 2 +-
.../tests/wp_usage/oracle/global.2.res.oracle | 2 +-
.../oracle/issue-189-bis.1.res.oracle | 2 +-
.../wp_usage/oracle/issue-189.2.res.oracle | 2 +-
.../wp_usage/oracle_qualif/caveat2.res.oracle | 2 +-
.../oracle_qualif/issue-189-bis.1.res.oracle | 2 +-
31 files changed, 100 insertions(+), 89 deletions(-)
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 0a8086800c9..1b1066105cb 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 1f183b1d30a..9c383998a35 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 43305903b45..e9a2a01d9a2 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 56bb306558b..5508bc18319 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 53078f53cb8..87430ad4b3c 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 3903ba3a3a3..174cfa75215 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 1dfeafb91d5..cfbc3114675 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 03056370c4a..30d6f05c1f7 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 380a7e0cc8a..142b8eba246 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 bf4453996e1..3d3946ce97f 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 b99e1013102..535d8556ba5 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 ab588be9a5c..66bc5879f09 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 6a5957ad9bc..da1d5866702 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 6fa2c547d93..c94049ea06d 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 3fba6a750b4..549d47287ee 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 541dd3c634a..1fe84b7fa72 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 828cc1502c5..b4246e6986e 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 e5d8aa84c06..24c245a193b 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 225a0af153d..a63862b2bf4 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 187f1b109f2..1f2fed4938b 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 7a7b1b25d56..24ac613e94a 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 e571b4fc2cc..26c949f5c0c 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 ad44942e79c..5d5ce1185b2 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 d37ff58f250..18eff921dea 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 7f6f4e13162..0141c03ea9f 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 bd126749ac2..7ec4d49d41a 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 3489aa28745..7bb8969a653 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 c15cbee10c3..0fb3ea0ed2e 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 5cd9f57c585..0114ddb6468 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 86f77567c02..5ebef0000b8 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 e73a38c074f..4a5c45145f6 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);
--
GitLab