[wp] frame conditions for compounds

# Conflicts:
#	src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
#	src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle

src/plugins/wp/MemVar.ml

@@ -913,6 +913,35 @@ struct
                     pretty l Vset.pp_bound a Vset.pp_bound b
         end
 
+  (* -------------------------------------------------------------------------- *)
+  (* ---  Framing                                                           --- *)
+  (* -------------------------------------------------------------------------- *)
+
+  let rec forall_pointers phi v t =
+    match Cil.unrollType t with
+    | TInt _ | TFloat _ | TVoid _ | TEnum _ | TNamed _ | TBuiltin_va_list _
+      -> F.p_true
+    | TPtr _ | TFun _ -> phi v
+    | TComp({ cfields },_,_) ->
+        F.p_all
+          (fun fd -> forall_pointers phi (e_getfield v (Cfield fd)) fd.ftype)
+          cfields
+    | TArray(elt,_,_,_) ->
+        let k = Lang.freshvar Qed.Logic.Int in
+        F.p_forall [k] (forall_pointers phi (e_get v (e_var k)) elt)
+
+  let frame sigma =
+    let hs = ref [] in
+    SIGMA.iter
+      (fun x chunk ->
+         if (x.vglob || x.vformal) then
+           let t = VAR.typ_of_chunk x in
+           let v = e_var chunk in
+           let h = forall_pointers (M.global sigma.mem) v t in
+           if not (F.eqp h F.p_true) then hs := h :: !hs
+      ) sigma.vars ;
+    !hs @ M.frame sigma.mem
+
   (* -------------------------------------------------------------------------- *)
   (* ---  Scope                                                             --- *)
   (* -------------------------------------------------------------------------- *)
@@ -926,15 +955,6 @@ struct
     | ByRef | InContext | InArray | NotUsed -> false
     | ByValue | ByShift | ByAddr -> true
 
-  let frame sigma =
-    let pool = ref [] in
-    SIGMA.iter
-      (fun x p ->
-         if (x.vglob || x.vformal) && Cil.isPointerType (VAR.typ_of_chunk x)
-         then pool := M.global sigma.mem (e_var p) :: !pool
-      ) sigma.vars ;
-    !pool @ M.frame sigma.mem
-
   let alloc sigma xs =
     let xm = List.filter is_mem xs in
     let mem = M.alloc sigma.mem xm in

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

@@ -46,16 +46,19 @@ Prove: EqS2_St(st0_0, st1_0).
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_acsl/equal.i, line 47) in 'with_ptr_and_array_struct':
-Let a = q0_0.F4_Q_qs.
-Let a_1 = q1_0.F4_Q_qs.
-Let a_2 = q0_0.F4_Q_qt.
-Let a_3 = q1_0.F4_Q_qt.
+Let a = q0_0.F4_Q_qp.
+Let a_1 = q1_0.F4_Q_qp.
+Let a_2 = q0_0.F4_Q_qs.
+Let a_3 = q1_0.F4_Q_qs.
+Let a_4 = q0_0.F4_Q_qt.
+Let a_5 = q1_0.F4_Q_qt.
 Assume {
-  Type: IsS4_Q(q0_0) /\ IsS4_Q(q1_0) /\ IsArray1_sint32(a_2) /\
-      IsArray1_sint32(a_3) /\ IsS1_S(a) /\ IsS1_S(a_1).
+  Type: IsS4_Q(q0_0) /\ IsS4_Q(q1_0) /\ IsArray1_sint32(a_4) /\
+      IsArray1_sint32(a_5) /\ IsS1_S(a_2) /\ IsS1_S(a_3).
   (* Goal *)
-  When: ((q1_0.F4_Q_qp) = (q0_0.F4_Q_qp)) /\ EqS1_S(a, a_1) /\
-      EqArray1_int(2, a_2, a_3).
+  When: (a_1 = a) /\ EqS1_S(a_2, a_3) /\ EqArray1_int(2, a_4, a_5).
+  (* Heap *)
+  Have: (region(a.base) <= 0) /\ (region(a_1.base) <= 0).
 }
 Prove: EqS4_Q(q0_0, q1_0).
 
@@ -68,6 +71,9 @@ Goal Post-condition (file tests/wp_acsl/equal.i, line 40) in 'with_ptr_array':
 Assume {
   (* Goal *)
   When: forall i : Z. ((0 <= i) -> ((i <= 4) -> (tp1_0[i] = tp0_0[i]))).
+  (* Heap *)
+  Have: (forall i : Z. region(tp0_0[i].base) <= 0) /\
+      (forall i : Z. region(tp1_0[i].base) <= 0).
 }
 Prove: EqArray1_pointer(5, tp0_0, tp1_0).
 
@@ -77,7 +83,14 @@ Prove: EqArray1_pointer(5, tp0_0, tp1_0).
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_acsl/equal.i, line 34) in 'with_ptr_struct':
-Assume { (* Goal *) When: (sp1_0.F3_Sp_p) = (sp0_0.F3_Sp_p). }
+Let a = sp0_0.F3_Sp_p.
+Let a_1 = sp1_0.F3_Sp_p.
+Assume {
+  (* Goal *)
+  When: a_1 = a.
+  (* Heap *)
+  Have: (region(a.base) <= 0) /\ (region(a_1.base) <= 0).
+}
 Prove: EqS3_Sp(sp0_0, sp1_0).
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle

@@ -205,7 +205,7 @@ Assume {
   (* Goal *)
   When: (0 <= i) /\ (i <= 4).
   (* Heap *)
-  Have: linked(Malloc_0).
+  Have: linked(Malloc_0) /\ (forall i_1 : Z. region(tps_0[i_1].base) <= 0).
   (* Pre-condition *)
   Have: valid_rw(Malloc_0, a_1, 10).
   (* Call 'reset_5' *)

src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle

@@ -26,6 +26,9 @@ Assume {
   Init: (a.F1_f) = global(G_e_22).
   (* Initializer *)
   Init: (a.F1_g) = global(G_f_23).
+  (* Heap *)
+  Have: forall i_1 : Z. let a_4 = A[i_1] in (region(a_4.F1_f.base) <= 0) /\
+      (region(a_4.F1_g.base) <= 0).
   (* Pre-condition *)
   Have: (0 <= i) /\ (i <= 2).
 }
@@ -46,6 +49,9 @@ Assume {
   Init: (A[1].F1_f) = a_1.
   (* Initializer *)
   Init: (A[2].F1_f) = a.
+  (* Heap *)
+  Have: forall i_1 : Z. let a_4 = A[i_1] in (region(a_4.F1_f.base) <= 0) /\
+      (region(a_4.F1_g.base) <= 0).
   (* Pre-condition *)
   Have: (0 <= i) /\ (i <= 2).
 }

src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle

@@ -255,7 +255,7 @@ Assume {
   Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 499) ->
       (p[i_1] = global(G_p0_28)))).
   (* Heap *)
-  Have: linked(Malloc_0).
+  Have: linked(Malloc_0) /\ (forall i_1 : Z. region(p[i_1].base) <= 0).
 }
 Prove: valid_rw(Malloc_0, p[i], 1).
 

src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle

@@ -11,7 +11,8 @@ Goal Assertion 'SEP' (file tests/wp_typed/frame.i, line 10):
 Assume {
   Type: is_sint32(k).
   (* Heap *)
-  Have: (region(Q.base) <= 0) /\ linked(Malloc_0).
+  Have: (region(Q.base) <= 0) /\ linked(Malloc_0) /\
+      (forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
   (* Pre-condition *)
   Have: (0 <= k) /\ (k <= 19).
 }
@@ -26,7 +27,8 @@ Let x = Mint_0[a <- 4][a_1].
 Assume {
   Type: is_sint32(k) /\ is_sint32(x).
   (* Heap *)
-  Have: (region(Q.base) <= 0) /\ linked(Malloc_0).
+  Have: (region(Q.base) <= 0) /\ linked(Malloc_0) /\
+      (forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
   (* Pre-condition *)
   Have: (0 <= k) /\ (k <= 19).
   (* Initializer *)

src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle

@@ -11,7 +11,8 @@ Goal Assertion 'SEP' (file tests/wp_typed/frame.i, line 10):
 Assume {
   Type: is_sint32(k).
   (* Heap *)
-  Have: (region(Q.base) <= 0) /\ linked(Malloc_0).
+  Have: (region(Q.base) <= 0) /\ linked(Malloc_0) /\
+      (forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
   (* Pre-condition *)
   Have: (0 <= k) /\ (k <= 19).
 }
@@ -26,7 +27,8 @@ Let x = Mint_0[a <- 4][a_1].
 Assume {
   Type: is_sint32(k) /\ is_sint32(x).
   (* Heap *)
-  Have: (region(Q.base) <= 0) /\ linked(Malloc_0).
+  Have: (region(Q.base) <= 0) /\ linked(Malloc_0) /\
+      (forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
   (* Pre-condition *)
   Have: (0 <= k) /\ (k <= 19).
   (* Initializer *)

src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle

@@ -4,12 +4,12 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_compound_assert_SEP : Unsuccess
+[wp] [Alt-Ergo 2.0.0] Goal typed_compound_assert_SEP : Valid
 [wp] [Alt-Ergo 2.0.0] Goal typed_compound_assert_RES : Valid
-[wp] Proved goals:    1 / 2
+[wp] Proved goals:    2 / 2
   Qed:               0 
-  Alt-Ergo 2.0.0:    1  (unsuccess: 1)
+  Alt-Ergo 2.0.0:    2
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  compound                  -        1        2      50.0%
+  compound                  -        2        2       100%
 ------------------------------------------------------------