diff --git a/src/plugins/wp/MemAddr.ml b/src/plugins/wp/MemAddr.ml
index a043d41b134bd872e4b49c34efb7157def92c93d..aa8002f34043209313eb192813fcf2432bd1d737 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"
@@ -79,6 +78,8 @@ let p_linked = Lang.extern_fp ~coloring:true ~library "linked"
(* --- API --- *)
(* -------------------------------------------------------------------------- *)
+(* Basic constructors and getters *)
+
let base addr = e_fun f_base [ addr ]
let offset addr = e_fun f_offset [ addr ]
let null = constant (e_fun f_null [])
@@ -86,25 +87,45 @@ let global base = e_fun f_global [ base ]
let shift addr offset = e_fun f_shift [ addr ; offset ]
let mk_addr base offset = shift (global base) offset
+(* Comparisons *)
+
let addr_lt addr1 addr2 = p_call p_addr_lt [ addr1 ; addr2 ]
let addr_le addr1 addr2 = p_call p_addr_le [ addr1 ; addr2 ]
+(* Regions *)
+
+let region base = e_fun f_region [ base ]
+let linked memory = p_call p_linked [ memory ]
+
+(* Validity *)
+
+let valid_rd alloc addr size = p_call p_valid_rd [ alloc ; addr ; size ]
+let valid_rw alloc addr size = p_call p_valid_rw [ alloc ; addr ; size ]
+let valid_obj alloc addr size = p_call p_valid_obj [ alloc ; addr ; size ]
+let invalid alloc addr size = p_call p_invalid [ alloc ; addr ; size ]
+
+(* Physical addresses *)
+
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 static_alloc 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 [ static_alloc @@ base addr ] @@
+ Cint.range (Ctypes.c_ptr ()) @@ int_of_addr addr
+
+(* Table of offsets *)
+
let base_offset base offset =
let offset_index = e_fun f_table_of_base [base] in
e_fun f_table_to_offset [offset_index ; offset]
(** Returns the offset in {i bytes} from the {i logic} offset
(which is a memory cell index, actually) *)
-let valid_rd alloc addr size = p_call p_valid_rd [ alloc ; addr ; size ]
-let valid_rw alloc addr size = p_call p_valid_rw [ alloc ; addr ; size ]
-let valid_obj alloc addr size = p_call p_valid_obj [ alloc ; addr ; size ]
-let invalid alloc addr size = p_call p_invalid [ alloc ; addr ; size ]
-
-let region base = e_fun f_region [ base ]
-let linked memory = p_call p_linked [ memory ]
(* -------------------------------------------------------------------------- *)
(* --- Qed Simplifiers --- *)
@@ -293,10 +314,7 @@ let phi_int_of_addr p =
| _ -> raise Not_found
let phi_addr_of_int p =
- if p == e_zero then null else
- match repr p with
- | Fun(f,[a]) when f == f_int_of_addr -> a
- | _ -> raise Not_found
+ if p == e_zero then null else raise Not_found
(* -------------------------------------------------------------------------- *)
(* --- Simplifier for (in)validity --- *)
diff --git a/src/plugins/wp/MemAddr.mli b/src/plugins/wp/MemAddr.mli
index 1b97aa438030a65e67c78b57361bfb5cbf94dc20..82271610e67fd6861224f2978e1b6a537746e8c1 100644
--- a/src/plugins/wp/MemAddr.mli
+++ b/src/plugins/wp/MemAddr.mli
@@ -52,12 +52,24 @@ val global : term -> term
val shift : term -> term -> term
(** [shift (a: addr) (k: int) : addr = { a with offset = a.offset + k } ]*)
+(** {2 Comparisons} *)
+
val addr_lt : term -> term -> pred
(** [addr_lt(a: addr) (b: addr) = a < b] *)
val addr_le : term -> term -> pred
(** [addr_le(a: addr) (b: addr) = a <= b] *)
+(** {2 Physical addresses} *)
+
+val static_alloc : term -> pred
+(** [statically_allocated (base: int)]
+ The base has an associated static allocation, guaranteeing that the
+ addresses that use this base can be translated to integers and back.
+
+ @since Frama-C+dev
+*)
+
val addr_of_int : term -> term
(** [addr_of_int(i: int) : addr]
Abstract: Conversion from integer to address
@@ -68,6 +80,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
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 f6022c775262af8b7f6ac271cd83966d28575984..200a8d7d9026e16d6187598ec28d23182c678b36 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
@@ -136,9 +136,29 @@ theory MemAddr
(* Physical Address *)
+ function static_malloc int : int
+
+ predicate statically_allocated (base: int) =
+ base = 0 \/ static_malloc base > 0
+
+ (* Note: for now, we cannot prove that but Why3 does not see that the function
+ 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)
+
function int_of_addr addr: int
function addr_of_int int: addr
+ axiom addr_of_null :
+ int_of_addr null = 0
+
+ axiom addr_of_int_bijection :
+ forall p:addr.
+ statically_allocated p.base -> addr_of_int (int_of_addr p) = p
+
+ (* Table of offsets *)
+
type table (* abstract for now, but can be more elaborated later on *)
function table_of_base int: table
function table_to_offset table int: int
@@ -150,13 +170,4 @@ theory MemAddr
forall t: table. forall o1 o2: int.
o1 <= o2 <-> table_to_offset t o1 <= table_to_offset t o2
- axiom int_of_addr_bijection :
- forall a:int. int_of_addr (addr_of_int a) = a
-
- axiom addr_of_int_bijection :
- forall p:addr. addr_of_int (int_of_addr p) = p
-
- axiom addr_of_null :
- int_of_addr null = 0
-
end
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
index 3299adf20a915453632ed478e54ca2589c6aa819..8d47908d4657c9a7cd58f220b5bfd81026b205de 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 4 [...]
+# frama-c -wp -wp-timeout 6 [...]
[kernel] Parsing user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] [Valid] Goal init_exits (Cfg) (Unreachable)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index 07bae8c292c0a86ee719864016baef469ecf12d0..eb17638ed86ab4b01bed32b454197b0fa4e0988e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -22,13 +22,13 @@
[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part2 (Tactics 2) (Qed 12/13) (Alt-Ergo 1/13) (Cached)
[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part3 (Tactics 3) (Qed 34/34)
[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part2 (Tactic) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part2 (Tactics 2) (Qed 12/13) (Alt-Ergo 1/13) (Cached)
[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part3 (Qed)
[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part2 (Tactic) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part2 (Tactics 2) (Qed 12/13) (Alt-Ergo 1/13) (Cached)
[wp] Proved goals: 23 / 23
Qed: 11
- Script: 12 (Tactics 23) (Qed 162/175) (Alt-Ergo 13/175) (Cached)
+ Script: 12 (Tactics 25) (Qed 186/197) (Alt-Ergo 11/197) (Cached)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init_t2_v2 3 - 8 100%
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index 37891a304ee359938feca32215d1221c0e0a2e9c..b43110aa3531fcb690015a60b7d1099fcd319c02 100644
--- a/src/plugins/wp/tests/wp_typed/user_init.i
+++ b/src/plugins/wp/tests/wp_typed/user_init.i
@@ -1,6 +1,6 @@
/* run.config_qualif
- OPT: -wp-prop=-lack,-tactic -wp-timeout 4
+ OPT: -wp-prop=-lack,-tactic -wp-timeout 6
OPT: -wp-prop=tactic -wp-auto=wp:split,wp:range -wp-prover=tip,Alt-Ergo -wp-script dry
OPT: -wp-prop=lack
*/