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 67%
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..e9495cd015d61cbc36a6d21a1de8a68a962f7ec0 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,21 +1,23 @@
# 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).
@@ -25,76 +27,91 @@ Prove: ((0 <= k) /\ (k <= 25)) <->
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).
------------------------------------------------------------
-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).
------------------------------------------------------------
-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).
------------------------------------------------------------
-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).
------------------------------------------------------------
-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), 2).
+
+------------------------------------------------------------
+
+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), 1).
+
------------------------------------------------------------
------------------------------------------------------------
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,36 +119,36 @@ 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).
------------------------------------------------------------
-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).
------------------------------------------------------------
-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).
------------------------------------------------------------
-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).
------------------------------------------------------------
-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).
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..0775d61de97766153e1f57cd1d61bef1cbb6112b 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,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_AM (Qed)
-[wp] Proved goals: 28 / 28
- Terminating: 4
- Unreachable: 4
+[wp] [Unsuccess] typed_dangling_check (Alt-Ergo) (Cached)
+[wp] Proved goals: 30 / 32
+ Terminating: 5
+ Unreachable: 5
Qed: 10
Alt-Ergo: 10
+ Unsuccess: 2
------------------------------------------------------------
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 4 10 90.0%
+ dangling - - 1 0.0%
------------------------------------------------------------