From 5b21f33e265b056ff72dee08b91ec23ab73a0348 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 2 Oct 2024 13:55:00 +0200
Subject: [PATCH] [wp] fix valid_obj for dangling pointers
---
src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw | 2 +-
.../wp_acsl/oracle_qualif/object_pointer.res.oracle | 9 ++++-----
2 files changed, 5 insertions(+), 6 deletions(-)
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 71842fd4ed8..4d86f2a53f0 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 9ca8cd79384..8bf988272c2 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%
------------------------------------------------------------
--
GitLab