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..bbce544b27c9f648061f32038f22daf6adcfb97d 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] /\ 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
@@ -145,7 +144,7 @@ theory MemAddr
statically allocated uses static_malloc which is abstract. *)
lemma valid_pointers_are_statically_allocated:
forall a: addr, m: malloc, n: int.
- valid_rd m a n -> statically_allocated (a.base)
+ n > 0 -> valid_rd m a n -> statically_allocated (a.base)
function int_of_addr addr: int
function addr_of_int int: addr
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/invalid_pointer.c b/src/plugins/wp/tests/wp_acsl/object_pointer.i
similarity index 89%
rename from src/plugins/wp/tests/wp_acsl/invalid_pointer.c
rename to src/plugins/wp/tests/wp_acsl/object_pointer.i
index b1e5a2f0f9ad8cd393ff689c00afb36926be0c0b..da0090d0999c7de0faaf954b2843d5b3362af37e 100644
--- a/src/plugins/wp/tests/wp_acsl/invalid_pointer.c
+++ b/src/plugins/wp/tests/wp_acsl/object_pointer.i
@@ -54,7 +54,17 @@ void compound(void)
//@check G: \object_pointer(&(p->g));
//@check F2: \object_pointer(&(p->f)+2);
//@check G2: !\object_pointer(&(p->g)+2);
+ //@check E: \object_pointer(p+1);
int k ;
struct A a ;
//@check AM: (0 <= k <= 10) <==> \object_pointer(&a.m[k]);
}
+
+void dangling(void){
+ int *p ;
+ {
+ int l ;
+ p = &l ;
+ }
+ //@ check !\object_pointer(p);
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle
similarity index 62%
rename from src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle
rename to src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle
index 6d5be83644c757be7ca3bd42dd13d2c66196aeb0..336c2664ae12b40d0ddbb5b6ec523110342a23b0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle
@@ -1,100 +1,117 @@
# frama-c -wp [...]
-[kernel] Parsing invalid_pointer.c (with preprocessing)
+[kernel] Parsing object_pointer.i (no preprocessing)
[wp] Running WP plugin...
[wp] [Valid] Goal array_exits (Cfg) (Unreachable)
[wp] [Valid] Goal array_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] [Valid] Goal compound_exits (Cfg) (Unreachable)
[wp] [Valid] Goal compound_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal dangling_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal dangling_terminates (Cfg) (Trivial)
[wp] [Valid] Goal memvar_exits (Cfg) (Unreachable)
[wp] [Valid] Goal memvar_terminates (Cfg) (Trivial)
[wp] [Valid] Goal pointer_exits (Cfg) (Unreachable)
[wp] [Valid] Goal pointer_terminates (Cfg) (Trivial)
-[wp] invalid_pointer.c:23: Warning: void object
+[wp] object_pointer.i:23: Warning: void object
------------------------------------------------------------
Function array
------------------------------------------------------------
-Goal Check 'ARR' (file invalid_pointer.c, line 32):
+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)).
------------------------------------------------------------
------------------------------------------------------------
Function compound
------------------------------------------------------------
-Goal Check 'M1' (file invalid_pointer.c, line 47):
+Goal Check 'M1' (file object_pointer.i, line 47):
Prove: true.
------------------------------------------------------------
-Goal Check 'P0' (file invalid_pointer.c, line 48):
+Goal Check 'P0' (file object_pointer.i, line 48):
Prove: true.
------------------------------------------------------------
-Goal Check 'P1' (file invalid_pointer.c, line 49):
+Goal Check 'P1' (file object_pointer.i, line 49):
Prove: true.
------------------------------------------------------------
-Goal Check 'P2' (file invalid_pointer.c, line 50):
+Goal Check 'P2' (file object_pointer.i, line 50):
Prove: true.
------------------------------------------------------------
-Goal Check 'F' (file invalid_pointer.c, line 53):
+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 invalid_pointer.c, line 54):
+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 invalid_pointer.c, line 55):
+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 invalid_pointer.c, line 56):
+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 'AM' (file invalid_pointer.c, line 59):
+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)).
+
+------------------------------------------------------------
+
+Goal Check 'AM' (file object_pointer.i, line 60):
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function dangling
+------------------------------------------------------------
+
+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)).
+
------------------------------------------------------------
------------------------------------------------------------
Function memvar
------------------------------------------------------------
-Goal Check 'M1' (file invalid_pointer.c, line 6):
+Goal Check 'M1' (file object_pointer.i, line 6):
Prove: true.
------------------------------------------------------------
-Goal Check 'P0' (file invalid_pointer.c, line 7):
+Goal Check 'P0' (file object_pointer.i, line 7):
Prove: true.
------------------------------------------------------------
-Goal Check 'P1' (file invalid_pointer.c, line 8):
+Goal Check 'P1' (file object_pointer.i, line 8):
Prove: true.
------------------------------------------------------------
-Goal Check 'P2' (file invalid_pointer.c, line 9):
+Goal Check 'P2' (file object_pointer.i, line 9):
Prove: true.
------------------------------------------------------------
@@ -102,37 +119,37 @@ Prove: true.
Function pointer
------------------------------------------------------------
-Goal Check 'M1' (file invalid_pointer.c, line 19):
+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 invalid_pointer.c, line 20):
+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 invalid_pointer.c, line 21):
+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 invalid_pointer.c, line 22):
+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)).
------------------------------------------------------------
-Goal Check 'qed_NULL' (file invalid_pointer.c, line 23):
+Goal Check 'qed_NULL' (file object_pointer.i, line 23):
Prove: true.
------------------------------------------------------------
-Goal Check 'prover_NULL' (file invalid_pointer.c, line 24):
+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/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle
similarity index 77%
rename from src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
rename to src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle
index 4090d279a5e1f3cacdc3ab941df1af9a455b36c0..8bf988272c25034b8417935ec42c9c4e6b3582b4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle
@@ -1,17 +1,19 @@
# frama-c -wp [...]
-[kernel] Parsing invalid_pointer.c (with preprocessing)
+[kernel] Parsing object_pointer.i (no preprocessing)
[wp] Running WP plugin...
[wp] [Valid] Goal array_exits (Cfg) (Unreachable)
[wp] [Valid] Goal array_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] [Valid] Goal compound_exits (Cfg) (Unreachable)
[wp] [Valid] Goal compound_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal dangling_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal dangling_terminates (Cfg) (Trivial)
[wp] [Valid] Goal memvar_exits (Cfg) (Unreachable)
[wp] [Valid] Goal memvar_terminates (Cfg) (Trivial)
[wp] [Valid] Goal pointer_exits (Cfg) (Unreachable)
[wp] [Valid] Goal pointer_terminates (Cfg) (Trivial)
-[wp] invalid_pointer.c:23: Warning: void object
-[wp] 20 goals scheduled
+[wp] object_pointer.i:23: Warning: void object
+[wp] 22 goals scheduled
[wp] [Valid] typed_memvar_check_M1 (Qed)
[wp] [Valid] typed_memvar_check_P0 (Qed)
[wp] [Valid] typed_memvar_check_P1 (Qed)
@@ -31,16 +33,19 @@
[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] [Valid] typed_compound_check_E (Alt-Ergo) (Cached)
[wp] [Valid] typed_compound_check_AM (Qed)
-[wp] Proved goals: 28 / 28
- Terminating: 4
- Unreachable: 4
+[wp] [Valid] typed_dangling_check (Alt-Ergo) (Cached)
+[wp] Proved goals: 32 / 32
+ Terminating: 5
+ Unreachable: 5
Qed: 10
- Alt-Ergo: 10
+ Alt-Ergo: 12
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
memvar 4 - 4 100%
pointer 1 5 6 100%
array - 1 1 100%
- compound 5 4 9 100%
+ compound 5 5 10 100%
+ dangling - 1 1 100%
------------------------------------------------------------