From facbbb73f5c9a05a2ada801bee51fd73fc70712a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 2 Oct 2024 13:55:55 +0200
Subject: [PATCH] [wp] add a guard to statically_allocated
---
src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
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 4d86f2a53f0..bbce544b27c 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
@@ -144,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
--
GitLab