diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index c508fdae4430875422c5b95bf05b22ee7ee7c4ef..5489e17e49d787d04935ebad98966e6a93492373 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -111,7 +111,7 @@ theory Memory
predicate linked (map int int)
predicate sconst (map addr int)
predicate framed (m : map addr addr) =
- forall p:addr [m[p]]. region(m[p].base) <= 0
+ forall p:addr [m[p]]. region(p.base) <= 0 -> region(m[p].base) <= 0
(* Properties *)
diff --git a/src/plugins/wp/tests/wp_typed/frame.i b/src/plugins/wp/tests/wp_typed/frame.i
index 8620e34f2bb24650bde00799389b3538b1873e77..c68f9d167b32f1d59941b6596759c096877c44c6 100644
--- a/src/plugins/wp/tests/wp_typed/frame.i
+++ b/src/plugins/wp/tests/wp_typed/frame.i
@@ -14,3 +14,23 @@ void compound(int k) {
// NOTE:
// if we require \valid(comp[k].ptr) the goal is provable without frame conditions
// since it can not be aliased with 'm' at PRE, which is not (yet) valid.
+
+// For those two examples, we want the assert false to fail:
+// -> the frame condition must *not* introduce incoherence on initialization
+
+void local_region(void) {
+ char b[4] = {0};
+ char *x = b ;
+ char **in_memtyped = &x ; // be sure to put x in MemTyped
+ //@ assert A:X: \valid_read(x + (0..3));
+ //@ assert A:Y: \false ;
+}
+
+struct S { char b ; };
+
+void formal_region(struct S s) {
+ char *x = &s.b ;
+ char **in_memtyped = &x ; // be sure to put x in MemTyped
+ //@ assert A:X: \valid_read(x);
+ //@ assert A:Y: \false ;
+}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
index e433d6edd6b606562cedf393f35702bd4766e830..64b8f12db9b92dfb7f4ea35a80a51d9f671d3554 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
@@ -38,3 +38,61 @@ Assume {
Prove: x = 1.
------------------------------------------------------------
+------------------------------------------------------------
+ Function formal_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 34):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shiftfield_F2_S_b(global(P_s_36)).
+}
+Prove: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 35):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shiftfield_F2_S_b(global(P_s_36)).
+ (* Assertion 'A,X' *)
+ Have: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function local_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 25):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shift_sint8(global(L_b_31), 0).
+}
+Prove: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 26):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shift_sint8(global(L_b_31), 0).
+ (* Assertion 'A,X' *)
+ Have: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
index f958319c4c3c3f1942c23f3daaab8c2ce5ee627f..d1ace9a6829158bc2363250a76b8f34c86d26da7 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
@@ -38,3 +38,61 @@ Assume {
Prove: x = 1.
------------------------------------------------------------
+------------------------------------------------------------
+ Function formal_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 34):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shiftfield_F2_S_b(global(P_s_36)).
+}
+Prove: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 35):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shiftfield_F2_S_b(global(P_s_36)).
+ (* Assertion 'A,X' *)
+ Have: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function local_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 25):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shift_sint8(global(L_b_31), 0).
+}
+Prove: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 26):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shift_sint8(global(L_b_31), 0).
+ (* Assertion 'A,X' *)
+ Have: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
index 96bb1c3037c84b0974790f377c051aa0257fd6fa..991ca84c401b93c81cf2fca1747872a72766cc92 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
@@ -2,13 +2,19 @@
[kernel] Parsing tests/wp_typed/frame.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
+[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_compound_assert_SEP : Unsuccess
[wp] [Alt-Ergo] Goal typed_compound_assert_RES : Valid
-[wp] Proved goals: 1 / 2
+[wp] [Alt-Ergo] Goal typed_local_region_assert_A_X : Valid
+[wp] [Alt-Ergo] Goal typed_local_region_assert_A_Y : Unsuccess
+[wp] [Alt-Ergo] Goal typed_formal_region_assert_A_X : Valid
+[wp] [Alt-Ergo] Goal typed_formal_region_assert_A_Y : Unsuccess
+[wp] Proved goals: 3 / 6
Qed: 0
- Alt-Ergo: 1 (unsuccess: 1)
+ Alt-Ergo: 3 (unsuccess: 3)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
compound - 1 2 50.0%
+ local_region - 1 2 50.0%
+ formal_region - 1 2 50.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
index d6b2be2c19d0a3c9227fced20293f93102d3d5bc..a187150cc649f2fe0559e01565b0547de2fada18 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0109,
+ "verdict": "valid", "time": 0.0088,
"steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0114,
+ "verdict": "valid", "time": 0.0116,
"steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
index d6b2be2c19d0a3c9227fced20293f93102d3d5bc..a187150cc649f2fe0559e01565b0547de2fada18 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0109,
+ "verdict": "valid", "time": 0.0088,
"steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0114,
+ "verdict": "valid", "time": 0.0116,
"steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index df90f71b8c97a99931e505509ad421ffe9e78911..baf7c5bf62b542aa313b0d746286e799b93e67b8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0151,
+ "verdict": "valid", "time": 0.0279,
"steps": 41 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0147,
+ "verdict": "valid", "time": 0.021,
"steps": 41 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index ab6c0d166bbb3cbc8605279fe510b720a5b8f879..cae89d2a942aa4f3f67bfeab7a4b6962d46fc0a4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0115,
+ "verdict": "valid", "time": 0.009,
"steps": 29 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0117,
+ "verdict": "valid", "time": 0.0131,
"steps": 29 } ] } } ]