diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index e91550d73ce8f894c5cca0eb32cfc0b4143558bd..912a953c52361b8f1fef5a3fcead37e0a9ceec3d 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -76,7 +76,8 @@ theory Memory
n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
predicate valid_obj (m : map int int) (p:addr) (n:int) =
- n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] )
+ n > 0 -> ( p = null \/
+ ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] ))
predicate invalid (m : map int int) (p:addr) (n:int) =
n > 0 -> ( m[p.base] <= p.offset \/ p.offset + n <= 0 )
diff --git a/src/plugins/wp/tests/wp_acsl/invalid_pointer.c b/src/plugins/wp/tests/wp_acsl/invalid_pointer.c
new file mode 100644
index 0000000000000000000000000000000000000000..14e08fdd4b9061d204f19f7699b5b58dea6492e8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/invalid_pointer.c
@@ -0,0 +1,57 @@
+/* Tests for \object_pointer() */
+
+void memvar(void)
+{
+ int x;
+ //@check M1: !\object_pointer(&x-1);
+ //@check P0: \object_pointer(&x);
+ //@check P1: \object_pointer(&x+1);
+ //@check P2: !\object_pointer(&x+2);
+}
+
+void pointer(void)
+{
+ int x;
+ int *p = &x ;
+ *p = 1 ;
+ //@check M1: !\object_pointer(p-1);
+ //@check P0: \object_pointer(p);
+ //@check P1: \object_pointer(p+1);
+ //@check P2: !\object_pointer(p+2);
+ //@check NULL: \object_pointer(\null);
+}
+
+void array(void)
+{
+ int k;
+ int a[25];
+ int *q = &a[k];
+ //@check ARR: (0 <= k <= 25) <==> \object_pointer(q);
+}
+
+struct S {
+ int f ;
+ int g ;
+};
+
+struct A {
+ int m[10];
+};
+
+void compound(void)
+{
+ struct S u ;
+ //@check M1: !\object_pointer(&u-1);
+ //@check P0: \object_pointer(&u);
+ //@check P1: \object_pointer(&u+1);
+ //@check P2: !\object_pointer(&u+2);
+ struct S s ;
+ struct S *p = &s ;
+ //@check F: \object_pointer(&(p->f));
+ //@check G: \object_pointer(&(p->g));
+ //@check F2: \object_pointer(&(p->f)+2);
+ //@check G2: !\object_pointer(&(p->g)+2);
+ int k ;
+ struct A a ;
+ //@check AM: (0 <= k <= 10) <==> \object_pointer(&a.m[k]);
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f1bb59e94b46d298d0042efddae2e4398c206640
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle
@@ -0,0 +1,126 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object
+------------------------------------------------------------
+ Function array
+------------------------------------------------------------
+
+Goal Check 'ARR' (file tests/wp_acsl/invalid_pointer.c, line 29):
+Assume { Type: is_sint32(k). (* Heap *) Type: linked(Malloc_0). }
+Prove: ((0 <= k) /\ (k <= 25)) <->
+ valid_obj(Malloc_0[L_a_32 <- 25], shift_sint32(global(L_a_32), k), 1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function compound
+------------------------------------------------------------
+
+Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 44):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 45):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P1' (file tests/wp_acsl/invalid_pointer.c, line 46):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 47):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'F' (file tests/wp_acsl/invalid_pointer.c, line 50):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_s_37 <- 2], shiftfield_F1_S_f(global(L_s_37)), 1).
+
+------------------------------------------------------------
+
+Goal Check 'G' (file tests/wp_acsl/invalid_pointer.c, line 51):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_s_37 <- 2], shiftfield_F1_S_g(global(L_s_37)), 1).
+
+------------------------------------------------------------
+
+Goal Check 'F2' (file tests/wp_acsl/invalid_pointer.c, line 52):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_s_37 <- 2],
+ shift_sint32(shiftfield_F1_S_f(global(L_s_37)), 2), 1).
+
+------------------------------------------------------------
+
+Goal Check 'G2' (file tests/wp_acsl/invalid_pointer.c, line 53):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: !valid_obj(Malloc_0[L_s_37 <- 2],
+ shift_sint32(shiftfield_F1_S_g(global(L_s_37)), 2), 1).
+
+------------------------------------------------------------
+
+Goal Check 'AM' (file tests/wp_acsl/invalid_pointer.c, line 56):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function memvar
+------------------------------------------------------------
+
+Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 7):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P1' (file tests/wp_acsl/invalid_pointer.c, line 8):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 9):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function pointer
+------------------------------------------------------------
+
+Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 17):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: !valid_obj(Malloc_0[L_x_27 <- 1], shift_sint32(global(L_x_27), -1), 1).
+
+------------------------------------------------------------
+
+Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 18):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_x_27 <- 1], global(L_x_27), 1).
+
+------------------------------------------------------------
+
+Goal Check 'P1' (file tests/wp_acsl/invalid_pointer.c, line 19):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_x_27 <- 1], shift_sint32(global(L_x_27), 1), 1).
+
+------------------------------------------------------------
+
+Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 20):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: !valid_obj(Malloc_0[L_x_27 <- 1], shift_sint32(global(L_x_27), 2), 1).
+
+------------------------------------------------------------
+
+Goal Check 'NULL' (file tests/wp_acsl/invalid_pointer.c, line 21):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_x_27 <- 1], null, 1).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/546d68cf73aa7d1be7397f0dba7ab57b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/546d68cf73aa7d1be7397f0dba7ab57b.json
new file mode 100644
index 0000000000000000000000000000000000000000..d824319ad4ad22a46757d91018cf5a68fc23e00f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/546d68cf73aa7d1be7397f0dba7ab57b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0104,
+ "steps": 15 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/6135a695451f38570cc5e98d983b3fc5.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/6135a695451f38570cc5e98d983b3fc5.json
new file mode 100644
index 0000000000000000000000000000000000000000..73bc5ac39eb7c96b55b0fc5ad096389816010c9e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/6135a695451f38570cc5e98d983b3fc5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0128,
+ "steps": 10 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/82fda005a00dfb2bafda2e7a61e31a0e.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/82fda005a00dfb2bafda2e7a61e31a0e.json
new file mode 100644
index 0000000000000000000000000000000000000000..c84d43dcd686f6fce0fb7e339c64fef178805708
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/82fda005a00dfb2bafda2e7a61e31a0e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0105,
+ "steps": 15 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a09f29e9995f66e54188484d0f6a022c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a09f29e9995f66e54188484d0f6a022c.json
new file mode 100644
index 0000000000000000000000000000000000000000..518bcc1fe1c38a5dee6ee6f3660ac7b6177deaf5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a09f29e9995f66e54188484d0f6a022c.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.01, "steps": 14 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a1789ac93bbdd1b61d2668d397e828b5.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a1789ac93bbdd1b61d2668d397e828b5.json
new file mode 100644
index 0000000000000000000000000000000000000000..bcc741b8f326f28cb37bd3b139bc1ca5cce32f4b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a1789ac93bbdd1b61d2668d397e828b5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0087,
+ "steps": 8 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a66c1f9591316a451c831ed9aa33375a.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a66c1f9591316a451c831ed9aa33375a.json
new file mode 100644
index 0000000000000000000000000000000000000000..41a0ec6c82063b9ccb0ed747ad2bb9fa3e1dc091
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a66c1f9591316a451c831ed9aa33375a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0099,
+ "steps": 10 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/bff665fbed54b18d00114b87eaddf2d7.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/bff665fbed54b18d00114b87eaddf2d7.json
new file mode 100644
index 0000000000000000000000000000000000000000..46a81b1550229c7211af35d36f932ca6671ccd23
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/bff665fbed54b18d00114b87eaddf2d7.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0149,
+ "steps": 22 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/e73bf6bee511f053358c2e0d3561a7e1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/e73bf6bee511f053358c2e0d3561a7e1.json
new file mode 100644
index 0000000000000000000000000000000000000000..d4e438038a9c53e3f3a69f85606d474e2924b985
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/e73bf6bee511f053358c2e0d3561a7e1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0116,
+ "steps": 15 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/edc73eb8a8cf742d31cbce5dfed79215.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/edc73eb8a8cf742d31cbce5dfed79215.json
new file mode 100644
index 0000000000000000000000000000000000000000..5a8ea347aa4ffe9098294ec81942688f852a5171
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/edc73eb8a8cf742d31cbce5dfed79215.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0106,
+ "steps": 16 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/f957b00472bc5ec2c8193749f227c435.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/f957b00472bc5ec2c8193749f227c435.json
new file mode 100644
index 0000000000000000000000000000000000000000..1731ee7379687e621f7b9ba0258a69da092e430a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/f957b00472bc5ec2c8193749f227c435.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.01, "steps": 11 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..600fdf9a79bf6be04ab2a6f2959a82199c5e350f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
@@ -0,0 +1,36 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object
+[wp] 19 goals scheduled
+[wp] [Alt-Ergo] Goal typed_array_check_ARR : Valid
+[wp] [Qed] Goal typed_compound_check_M1 : Valid
+[wp] [Qed] Goal typed_compound_check_P0 : Valid
+[wp] [Qed] Goal typed_compound_check_P1 : Valid
+[wp] [Qed] Goal typed_compound_check_P2 : Valid
+[wp] [Alt-Ergo] Goal typed_compound_check_F : Valid
+[wp] [Alt-Ergo] Goal typed_compound_check_G : Valid
+[wp] [Alt-Ergo] Goal typed_compound_check_F2 : Valid
+[wp] [Alt-Ergo] Goal typed_compound_check_G2 : Valid
+[wp] [Qed] Goal typed_compound_check_AM : Valid
+[wp] [Qed] Goal typed_memvar_check_M1 : Valid
+[wp] [Qed] Goal typed_memvar_check_P0 : Valid
+[wp] [Qed] Goal typed_memvar_check_P1 : Valid
+[wp] [Qed] Goal typed_memvar_check_P2 : Valid
+[wp] [Alt-Ergo] Goal typed_pointer_check_M1 : Valid
+[wp] [Alt-Ergo] Goal typed_pointer_check_P0 : Valid
+[wp] [Alt-Ergo] Goal typed_pointer_check_P1 : Valid
+[wp] [Alt-Ergo] Goal typed_pointer_check_P2 : Valid
+[wp] [Alt-Ergo] Goal typed_pointer_check_NULL : Valid
+[wp] Proved goals: 19 / 19
+ Qed: 9
+ Alt-Ergo: 10
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ memvar 4 - 4 100%
+ pointer - 5 5 100%
+ array - 1 1 100%
+ compound 5 4 9 100%
+------------------------------------------------------------