From 483c2982d0087aa24c136cc275ce2684fc526c53 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 20 Sep 2024 16:20:12 +0200
Subject: [PATCH] [wp] provide a function for pointers range
---
src/plugins/wp/MemAddr.ml | 12 ++++++++++--
src/plugins/wp/MemAddr.mli | 11 +++++++++++
2 files changed, 21 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/MemAddr.ml b/src/plugins/wp/MemAddr.ml
index 3ade44f81ba..9a687ca5e9d 100644
--- a/src/plugins/wp/MemAddr.ml
+++ b/src/plugins/wp/MemAddr.ml
@@ -49,13 +49,12 @@ let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
let f_addr_of_int = Lang.extern_f
- ~category:Qed.Logic.Injection
~library ~result:t_addr "addr_of_int"
let f_int_of_addr = Lang.extern_f
- ~category:Qed.Logic.Injection
~library ~result:Qed.Logic.Int "int_of_addr"
+let p_statically_allocated = Lang.extern_fp ~library "statically_allocated"
let f_table_of_base = Lang.extern_f ~library
~category:Qed.Logic.Function ~result:t_table "table_of_base"
@@ -110,6 +109,15 @@ let invalid alloc addr size = p_call p_invalid [ alloc ; addr ; size ]
let addr_of_int i = e_fun f_addr_of_int [ i ]
let int_of_addr addr = e_fun f_int_of_addr [ addr ]
+let statically_allocated addr = p_call p_statically_allocated [ addr ]
+(* This last function is not exposed, it does not have a particular meaning in
+ ACSL, and is used only for int/addr conversions.
+*)
+
+let in_uintptr_range addr =
+ p_hyps [ statically_allocated @@ base addr ] @@
+ Cint.range (Ctypes.c_ptr ()) @@ int_of_addr addr
+
(* Table of offsets *)
let base_offset base offset =
diff --git a/src/plugins/wp/MemAddr.mli b/src/plugins/wp/MemAddr.mli
index 1b97aa43803..8bfc3a3fbb0 100644
--- a/src/plugins/wp/MemAddr.mli
+++ b/src/plugins/wp/MemAddr.mli
@@ -68,6 +68,17 @@ val int_of_addr : term -> term
Abstract: Conversion from address to integer
*)
+val in_uintptr_range : term -> pred
+(** [in_uintptr_range (a: addr)] =
+ [statically_allocated(a.base) -> in_range(int_of_addr a)]
+
+ Assuming that the base of a statically exists, the conversion of the pointer
+ to a an integer produces a value that fits in [uintptr_t].
+
+ @since Frama-C+dev
+*)
+
+
val base_offset : term -> term -> term
(** [base_offset(base: int)(offset: int) : int]
Converts a {i logic} offset (which is actually the address of a memory cell
--
GitLab