[wp] Make sure that init are dispatched to MemTyped when needed

src/plugins/wp/MemVar.ml

@@ -1085,11 +1085,11 @@ struct
           | Ref _ -> p_true
           | Loc l -> M.initialized sigma.mem (Rloc(obj,l))
           | Val(m,x,p) ->
-              if (x.vformal || x.vglob) then
+              if is_heap_allocated m then
+                M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
+              else if (x.vformal || x.vglob) then
                 try valid_offset RW (vobject m x) p
                 with ShiftMismatch -> shift_mismatch l
-              else if is_heap_allocated m then
-                M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
               else
                 initialized_loc sigma obj x p
         end
@@ -1099,17 +1099,18 @@ struct
           | Loc l -> M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
           | Val(m,x,p) ->
               try
-                let in_array = valid_range RW (vobject m x) p (elt, a, b) in
-                let initialized =
-                  if x.vformal || x.vglob then p_true
-                  else initialized_range sigma (vobject m x) x p a b
-                in
-                F.p_imply (F.p_leq a b) (p_and in_array initialized)
-              with ShiftMismatch ->
                 if is_heap_allocated m then
                   let l = mloc_of_loc l in
                   M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
-                else shift_mismatch l
+                else
+                  let in_array = valid_range RW (vobject m x) p (elt, a, b) in
+                  let initialized =
+                    if x.vformal || x.vglob then p_true
+                    else initialized_range sigma (vobject m x) x p a b
+                  in
+                  F.p_imply (F.p_leq a b) (p_and in_array initialized)
+              with ShiftMismatch ->
+                shift_mismatch l
         end
     | Rrange(l, _,a,b) ->
         Warning.error
@@ -1191,7 +1192,8 @@ struct
     | Leave -> []
     | Enter ->
         let xs = List.filter
-            (fun v -> not v.vformal && not v.vglob && not v.vdefined) xs
+            (fun v -> is_mvar_alloc v && not v.vformal &&
+                      not v.vglob && not v.vdefined) xs
         in
         let uninitialized v =
           let value = Cvalues.uninitialized_obj (Ctypes.object_of v.vtype) in

src/plugins/wp/tests/wp_acsl/initialized_memtyped.i

@@ -81,4 +81,10 @@ void formal(int x)
 {
 	int * p = &x ;
 	//@ assert provable: \initialized(p);
-}
\ No newline at end of file
+}
+
+void ptr_on_local(void){
+  int x[3] = {0} ;
+  int *p = x ;
+  //@ assert provable: \initialized(p + (0..2));
+}

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

@@ -50,6 +50,26 @@ Goal Post-condition 'unknown' in 'glob_var':
 Assume { (* Heap *) Type: (region(px_0.base) <= 0) /\ cinits(Init_0). }
 Prove: (Init_0[px_0]=true).
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function ptr_on_local
+------------------------------------------------------------
+
+Goal Assertion 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 89):
+Let a = global(L_x_63).
+Assume {
+  (* Heap *)
+  Type: cinits(Init_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 2).
+  (* Initializer *)
+  Init: (Init_0[shift_sint32(a, 0)]=true).
+  (* Initializer *)
+  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+      (Init_0[shift_sint32(a, i_1)]=true))).
+}
+Prove: (Init_0[shift_sint32(a, i)]=true).
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function test

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

@@ -6,8 +6,8 @@
 [wp] [Qed] Goal typed_l_int_assert_SUCCS : Valid
 [wp] [Qed] Goal typed_l_int_assert_SUCCS_2 : Valid
 [wp] [Alt-Ergo] Goal typed_l_int_check_FAILS : Unsuccess
-[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS : Valid (missing cache)
-[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS_2 : Valid (missing cache)
+[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS : Valid
+[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS_2 : Valid
 [wp] [Alt-Ergo] Goal typed_l_array_check_FAILS : Unsuccess
 [wp] [Qed] Goal typed_l_struct_assert_SUCCS : Valid
 [wp] [Qed] Goal typed_l_struct_assert_SUCCS_2 : Valid

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

@@ -2,7 +2,7 @@
 [kernel] Parsing tests/wp_acsl/initialized_memtyped.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 28 goals scheduled
+[wp] 29 goals scheduled
 [wp] [Alt-Ergo] Goal typed_test_check_unknown : Unsuccess
 [wp] [Alt-Ergo] Goal typed_test_check_unknown_2 : Unsuccess
 [wp] [Alt-Ergo] Goal typed_test_check_unknown_3 : Unsuccess
@@ -31,13 +31,15 @@
 [wp] [Alt-Ergo] Goal typed_glob_arr_ensures_provable : Valid
 [wp] [Alt-Ergo] Goal typed_glob_arr_ensures_unknown : Unsuccess
 [wp] [Alt-Ergo] Goal typed_formal_assert_provable : Valid
-[wp] Proved goals:   13 / 28
+[wp] [Alt-Ergo] Goal typed_ptr_on_local_assert_provable : Valid
+[wp] Proved goals:   14 / 29
   Qed:             6 
-  Alt-Ergo:        7  (unsuccess: 15)
+  Alt-Ergo:        8  (unsuccess: 15)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   test                      6        4       23      43.5%
   glob_var                  -        1        2      50.0%
   glob_arr                  -        1        2      50.0%
   formal                    -        1        1       100%
+  ptr_on_local              -        1        1       100%
 ------------------------------------------------------------