[wp] object_pointer does not depend on the type size

src/plugins/wp/MemAddr.ml

@@ -101,7 +101,7 @@ let linked memory = p_call p_linked [ memory ]
 
 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 valid_obj alloc addr = p_call p_valid_obj [ alloc ; addr ]
 let invalid alloc addr size = p_call p_invalid [ alloc ; addr ; size ]
 
 (* Physical addresses *)
@@ -334,7 +334,7 @@ let r_valid_unref = function
 
 (* - lemma valid_obj_null: forall m n. valid_obj m null n *)
 let r_valid_obj = function
-  | [_; p; _] when decide (e_eq p null) -> e_true
+  | [_; p] when decide (e_eq p null) -> e_true
   | _ -> raise Not_found
 
 (* - lemma invalid_null: forall m n p. p.base = 0 -> invalid m p n *)

src/plugins/wp/MemAddr.mli

@@ -105,8 +105,8 @@ val valid_rd : term -> term -> term -> pred
 val valid_rw : term -> term -> term -> pred
 (** [valid_rw(m: malloc)(a: addr)(l: length)] *)
 
-val valid_obj : term -> term -> term -> pred
-(** [valid_obj(m: malloc)(a: addr)(l: length)] *)
+val valid_obj : term -> term -> pred
+(** [valid_obj(m: malloc)(a: addr)] *)
 
 val invalid : term -> term -> term -> pred
 (** [invalid(m: malloc)(a: addr)(l: length)]

src/plugins/wp/MemTyped.ml

@@ -1126,7 +1126,7 @@ let s_valid sigma acs p n =
   let valid = match acs with
     | RW -> MemAddr.valid_rw
     | RD -> MemAddr.valid_rd
-    | OBJ -> MemAddr.valid_obj
+    | OBJ -> (fun m p _ -> MemAddr.valid_obj m p)
   in
   valid (Sigma.value sigma T_alloc) p n
 

src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw

@@ -70,9 +70,8 @@ theory MemAddr
   predicate valid_rd (m: malloc) (p: addr) (n: int) =
     n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
 
-  predicate valid_obj (m: malloc) (p: addr) (n: int) =
-    n > 0 -> ( p = null \/
-             ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] ))
+  predicate valid_obj (m: malloc) (p: addr) =
+    p = null \/ (0 <> p.base /\ 0 <= p.offset /\ p.offset <= m[p.base])
 
   predicate invalid (m : malloc) (p:addr) (n:int) =
     n <= 0 \/ p.base = 0 \/ m[p.base] <= p.offset \/ p.offset + n <= 0

src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle

@@ -30,7 +30,7 @@ File "spec_memory.why", line 49, characters 4-59:
 Goal valid_rw_null.
 Prover result is: Valid.
 
-File "spec_memory.why", line 52, characters 4-34:
+File "spec_memory.why", line 52, characters 4-30:
 Goal valid_obj_null.
 Prover result is: Valid.
 

src/plugins/wp/tests/why3/spec_memory.why

@@ -49,7 +49,7 @@ module Spec_memory
     forall m n p. p.base = 0 -> (n <= 0 <-> valid_rw m p n)
 
   goal valid_obj_null:
-    forall m n. valid_obj m null n
+    forall m. valid_obj m null
 
   (* included simplifier *)
   goal INC_P:

src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle

@@ -20,7 +20,7 @@
 Goal Check 'ARR' (file object_pointer.i, line 32):
 Assume { Type: is_sint32(k). (* Heap *) Type: linked(Malloc_0). }
 Prove: ((0 <= k) /\ (k <= 25)) <->
-    valid_obj(Malloc_0[L_a_33 <- 25], shift_sint32(global(L_a_33), k), 1).
+    valid_obj(Malloc_0[L_a_33 <- 25], shift_sint32(global(L_a_33), k)).
 
 ------------------------------------------------------------
 ------------------------------------------------------------
@@ -49,33 +49,33 @@ Prove: true.
 
 Goal Check 'F' (file object_pointer.i, line 53):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_f(global(L_s_38)), 1).
+Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_f(global(L_s_38))).
 
 ------------------------------------------------------------
 
 Goal Check 'G' (file object_pointer.i, line 54):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_g(global(L_s_38)), 1).
+Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_g(global(L_s_38))).
 
 ------------------------------------------------------------
 
 Goal Check 'F2' (file object_pointer.i, line 55):
 Assume { (* Heap *) Type: linked(Malloc_0). }
 Prove: valid_obj(Malloc_0[L_s_38 <- 2],
-         shift_sint32(shiftfield_F1_S_f(global(L_s_38)), 2), 1).
+         shift_sint32(shiftfield_F1_S_f(global(L_s_38)), 2)).
 
 ------------------------------------------------------------
 
 Goal Check 'G2' (file object_pointer.i, line 56):
 Assume { (* Heap *) Type: linked(Malloc_0). }
 Prove: !valid_obj(Malloc_0[L_s_38 <- 2],
-          shift_sint32(shiftfield_F1_S_g(global(L_s_38)), 2), 1).
+          shift_sint32(shiftfield_F1_S_g(global(L_s_38)), 2)).
 
 ------------------------------------------------------------
 
 Goal Check 'E' (file object_pointer.i, line 57):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_s_38 <- 2], shift_S1_S(global(L_s_38), 1), 2).
+Prove: valid_obj(Malloc_0[L_s_38 <- 2], shift_S1_S(global(L_s_38), 1)).
 
 ------------------------------------------------------------
 
@@ -89,7 +89,7 @@ Prove: true.
 
 Goal Check (file object_pointer.i, line 69):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: !valid_obj(Malloc_0[L_l_45 <- 0], global(L_l_45), 1).
+Prove: !valid_obj(Malloc_0[L_l_45 <- 0], global(L_l_45)).
 
 ------------------------------------------------------------
 ------------------------------------------------------------
@@ -121,25 +121,25 @@ Prove: true.
 
 Goal Check 'M1' (file object_pointer.i, line 19):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), -1), 1).
+Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), -1)).
 
 ------------------------------------------------------------
 
 Goal Check 'P0' (file object_pointer.i, line 20):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_x_28 <- 1], global(L_x_28), 1).
+Prove: valid_obj(Malloc_0[L_x_28 <- 1], global(L_x_28)).
 
 ------------------------------------------------------------
 
 Goal Check 'P1' (file object_pointer.i, line 21):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 1), 1).
+Prove: valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 1)).
 
 ------------------------------------------------------------
 
 Goal Check 'P2' (file object_pointer.i, line 22):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 2), 1).
+Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 2)).
 
 ------------------------------------------------------------
 
@@ -150,6 +150,6 @@ Prove: true.
 
 Goal Check 'prover_NULL' (file object_pointer.i, line 24):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_x_28 <- 1], L_GET, 1).
+Prove: valid_obj(Malloc_0[L_x_28 <- 1], L_GET).
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle

@@ -33,20 +33,20 @@
 [wp] [Valid] typed_compound_check_G (Alt-Ergo) (Cached)
 [wp] [Valid] typed_compound_check_F2 (Alt-Ergo) (Cached)
 [wp] [Valid] typed_compound_check_G2 (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_compound_check_E (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:   30 / 32
+[wp] Proved goals:   31 / 32
   Terminating:     5
   Unreachable:     5
   Qed:            10
-  Alt-Ergo:       10
-  Unsuccess:       2
+  Alt-Ergo:       11
+  Unsuccess:       1
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   memvar                    4        -        4       100%
   pointer                   1        5        6       100%
   array                     -        1        1       100%
-  compound                  5        4       10      90.0%
+  compound                  5        5       10       100%
   dangling                  -        -        1       0.0%
 ------------------------------------------------------------