diff --git a/src/plugins/wp/MemAddr.ml b/src/plugins/wp/MemAddr.ml
index aa8002f34043209313eb192813fcf2432bd1d737..8c8dd1fcb4c4e1bf8a217a849a7492bd2f266995 100644
--- a/src/plugins/wp/MemAddr.ml
+++ b/src/plugins/wp/MemAddr.ml
@@ -101,7 +101,7 @@ let linked memory = p_call p_linked [ memory ]
let valid_rd alloc addr size = p_call p_valid_rd [ alloc ; addr ; size ]
let valid_rw alloc addr size = p_call p_valid_rw [ alloc ; addr ; size ]
-let valid_obj alloc addr size = p_call p_valid_obj [ alloc ; addr ; size ]
+let valid_obj alloc addr = p_call p_valid_obj [ alloc ; addr ]
let invalid alloc addr size = p_call p_invalid [ alloc ; addr ; size ]
(* Physical addresses *)
@@ -334,7 +334,7 @@ let r_valid_unref = function
(* - lemma valid_obj_null: forall m n. valid_obj m null n *)
let r_valid_obj = function
- | [_; p; _] when decide (e_eq p null) -> e_true
+ | [_; p] when decide (e_eq p null) -> e_true
| _ -> raise Not_found
(* - lemma invalid_null: forall m n p. p.base = 0 -> invalid m p n *)
diff --git a/src/plugins/wp/MemAddr.mli b/src/plugins/wp/MemAddr.mli
index 82271610e67fd6861224f2978e1b6a537746e8c1..93685f13772ac7ec03564eb9d16ad48d67fdea22 100644
--- a/src/plugins/wp/MemAddr.mli
+++ b/src/plugins/wp/MemAddr.mli
@@ -105,8 +105,8 @@ val valid_rd : term -> term -> term -> pred
val valid_rw : term -> term -> term -> pred
(** [valid_rw(m: malloc)(a: addr)(l: length)] *)
-val valid_obj : term -> term -> term -> pred
-(** [valid_obj(m: malloc)(a: addr)(l: length)] *)
+val valid_obj : term -> term -> pred
+(** [valid_obj(m: malloc)(a: addr)] *)
val invalid : term -> term -> term -> pred
(** [invalid(m: malloc)(a: addr)(l: length)]
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 94ac99b8edb5dad241bf3164e1779607c2c5d17e..dbfafb02cb6d1ecd9e910710f2c3dd8f87f436a0 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -1126,7 +1126,7 @@ let s_valid sigma acs p n =
let valid = match acs with
| RW -> MemAddr.valid_rw
| RD -> MemAddr.valid_rd
- | OBJ -> MemAddr.valid_obj
+ | OBJ -> (fun m p _ -> MemAddr.valid_obj m p)
in
valid (Sigma.value sigma T_alloc) p n
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
index 200a8d7d9026e16d6187598ec28d23182c678b36..71842fd4ed8ea6a71fa2afa3c9d235456287aaee 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
@@ -70,9 +70,8 @@ theory MemAddr
predicate valid_rd (m: malloc) (p: addr) (n: int) =
n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
- predicate valid_obj (m: malloc) (p: addr) (n: int) =
- n > 0 -> ( p = null \/
- ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] ))
+ predicate valid_obj (m: malloc) (p: addr) =
+ p = null \/ (0 <> p.base /\ 0 <= p.offset /\ p.offset <= m[p.base])
predicate invalid (m : malloc) (p:addr) (n:int) =
n <= 0 \/ p.base = 0 \/ m[p.base] <= p.offset \/ p.offset + n <= 0
diff --git a/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle b/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
index 59c4d29e5141b97d61a0d69fad0343908e33160b..8042b6718bd438950d0a22364f56451cd41db2cc 100644
--- a/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
+++ b/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
@@ -30,7 +30,7 @@ File "spec_memory.why", line 49, characters 4-59:
Goal valid_rw_null.
Prover result is: Valid.
-File "spec_memory.why", line 52, characters 4-34:
+File "spec_memory.why", line 52, characters 4-30:
Goal valid_obj_null.
Prover result is: Valid.
diff --git a/src/plugins/wp/tests/why3/spec_memory.why b/src/plugins/wp/tests/why3/spec_memory.why
index 29d0887963627a29b9eb99bfac31337249e89fe4..bc4f6ec4d8770821658aba57e15afc2dfb891757 100644
--- a/src/plugins/wp/tests/why3/spec_memory.why
+++ b/src/plugins/wp/tests/why3/spec_memory.why
@@ -49,7 +49,7 @@ module Spec_memory
forall m n p. p.base = 0 -> (n <= 0 <-> valid_rw m p n)
goal valid_obj_null:
- forall m n. valid_obj m null n
+ forall m. valid_obj m null
(* included simplifier *)
goal INC_P:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle
index e9495cd015d61cbc36a6d21a1de8a68a962f7ec0..336c2664ae12b40d0ddbb5b6ec523110342a23b0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle
@@ -20,7 +20,7 @@
Goal Check 'ARR' (file object_pointer.i, line 32):
Assume { Type: is_sint32(k). (* Heap *) Type: linked(Malloc_0). }
Prove: ((0 <= k) /\ (k <= 25)) <->
- valid_obj(Malloc_0[L_a_33 <- 25], shift_sint32(global(L_a_33), k), 1).
+ valid_obj(Malloc_0[L_a_33 <- 25], shift_sint32(global(L_a_33), k)).
------------------------------------------------------------
------------------------------------------------------------
@@ -49,33 +49,33 @@ Prove: true.
Goal Check 'F' (file object_pointer.i, line 53):
Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_f(global(L_s_38)), 1).
+Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_f(global(L_s_38))).
------------------------------------------------------------
Goal Check 'G' (file object_pointer.i, line 54):
Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_g(global(L_s_38)), 1).
+Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_g(global(L_s_38))).
------------------------------------------------------------
Goal Check 'F2' (file object_pointer.i, line 55):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_obj(Malloc_0[L_s_38 <- 2],
- shift_sint32(shiftfield_F1_S_f(global(L_s_38)), 2), 1).
+ shift_sint32(shiftfield_F1_S_f(global(L_s_38)), 2)).
------------------------------------------------------------
Goal Check 'G2' (file object_pointer.i, line 56):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: !valid_obj(Malloc_0[L_s_38 <- 2],
- shift_sint32(shiftfield_F1_S_g(global(L_s_38)), 2), 1).
+ shift_sint32(shiftfield_F1_S_g(global(L_s_38)), 2)).
------------------------------------------------------------
Goal Check 'E' (file object_pointer.i, line 57):
Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_s_38 <- 2], shift_S1_S(global(L_s_38), 1), 2).
+Prove: valid_obj(Malloc_0[L_s_38 <- 2], shift_S1_S(global(L_s_38), 1)).
------------------------------------------------------------
@@ -89,7 +89,7 @@ Prove: true.
Goal Check (file object_pointer.i, line 69):
Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: !valid_obj(Malloc_0[L_l_45 <- 0], global(L_l_45), 1).
+Prove: !valid_obj(Malloc_0[L_l_45 <- 0], global(L_l_45)).
------------------------------------------------------------
------------------------------------------------------------
@@ -121,25 +121,25 @@ Prove: true.
Goal Check 'M1' (file object_pointer.i, line 19):
Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), -1), 1).
+Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), -1)).
------------------------------------------------------------
Goal Check 'P0' (file object_pointer.i, line 20):
Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_x_28 <- 1], global(L_x_28), 1).
+Prove: valid_obj(Malloc_0[L_x_28 <- 1], global(L_x_28)).
------------------------------------------------------------
Goal Check 'P1' (file object_pointer.i, line 21):
Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 1), 1).
+Prove: valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 1)).
------------------------------------------------------------
Goal Check 'P2' (file object_pointer.i, line 22):
Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 2), 1).
+Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 2)).
------------------------------------------------------------
@@ -150,6 +150,6 @@ Prove: true.
Goal Check 'prover_NULL' (file object_pointer.i, line 24):
Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_x_28 <- 1], L_GET, 1).
+Prove: valid_obj(Malloc_0[L_x_28 <- 1], L_GET).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle
index 0775d61de97766153e1f57cd1d61bef1cbb6112b..9ca8cd793848e43accddd6beeaf7907f1ff7be33 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle
@@ -33,20 +33,20 @@
[wp] [Valid] typed_compound_check_G (Alt-Ergo) (Cached)
[wp] [Valid] typed_compound_check_F2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_compound_check_G2 (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_compound_check_E (Alt-Ergo) (Cached)
+[wp] [Valid] typed_compound_check_E (Alt-Ergo) (Cached)
[wp] [Valid] typed_compound_check_AM (Qed)
[wp] [Unsuccess] typed_dangling_check (Alt-Ergo) (Cached)
-[wp] Proved goals: 30 / 32
+[wp] Proved goals: 31 / 32
Terminating: 5
Unreachable: 5
Qed: 10
- Alt-Ergo: 10
- Unsuccess: 2
+ Alt-Ergo: 11
+ Unsuccess: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
memvar 4 - 4 100%
pointer 1 5 6 100%
array - 1 1 100%
- compound 5 4 10 90.0%
+ compound 5 5 10 100%
dangling - - 1 0.0%
------------------------------------------------------------