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 71842fd4ed8ea6a71fa2afa3c9d235456287aaee..4d86f2a53f0970b6e563d3d3350a1e388596fc53 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
@@ -71,7 +71,7 @@ theory MemAddr
n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
predicate valid_obj (m: malloc) (p: addr) =
- p = null \/ (0 <> p.base /\ 0 <= p.offset /\ p.offset <= m[p.base])
+ p = null \/ (0 <> p.base /\ 0 <= p.offset /\ p.offset <= m[p.base] /\ m[p.base] > 0)
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/wp_acsl/oracle_qualif/object_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle
index 9ca8cd793848e43accddd6beeaf7907f1ff7be33..8bf988272c25034b8417935ec42c9c4e6b3582b4 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
@@ -35,18 +35,17 @@
[wp] [Valid] typed_compound_check_G2 (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: 31 / 32
+[wp] [Valid] typed_dangling_check (Alt-Ergo) (Cached)
+[wp] Proved goals: 32 / 32
Terminating: 5
Unreachable: 5
Qed: 10
- Alt-Ergo: 11
- Unsuccess: 1
+ Alt-Ergo: 12
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
memvar 4 - 4 100%
pointer 1 5 6 100%
array - 1 1 100%
compound 5 5 10 100%
- dangling - - 1 0.0%
+ dangling - 1 1 100%
------------------------------------------------------------