[wp] addr_of_int only works for existing bases

src/plugins/wp/MemAddr.ml

@@ -79,6 +79,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 +88,36 @@ 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 ]
 
+(* 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 +306,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                                        --- *)

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