[wp] fix valid_obj for dangling pointers

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

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%
 ------------------------------------------------------------