diff --git a/src/plugins/override_std/basic_blocks.ml b/src/plugins/override_std/basic_blocks.ml
index 2eee115c55d2604611b9c8455ad2bc5bee58cadb..633b0cb10fa6a6c52bcbe7801bccb851e2b4c671 100644
--- a/src/plugins/override_std/basic_blocks.ml
+++ b/src/plugins/override_std/basic_blocks.ml
@@ -50,10 +50,11 @@ let rec string_of_typ_aux = function
   | TPtr(t, _) -> "ptr_" ^ string_of_typ t
   | TEnum (ei, _) -> ei.ename
   | TComp (ci, _, _) -> ci.cname
-  | TArray (t, _, _, _) -> "arr_" ^ string_of_typ t
+  | TArray (t, Some e, _, _) ->
+    "arr" ^ (string_of_exp e) ^ "_" ^ string_of_typ t
   | _ -> assert false
 and string_of_typ t = string_of_typ_aux (Cil.unrollType t)
-
+and string_of_exp e = Format.asprintf "%a" Cil_printer.pp_exp e
 
 let size_var t value = {
   l_var_info = make_logic_var_local "__fc_len" t;
@@ -98,10 +99,37 @@ let tbuffer_range ?loc ptr len =
   let range = trange ?loc (Some (tinteger ?loc 0), Some last) in
   tplus ?loc ptr range
 
-let tunref_range ?loc ptr len =
+let rec tunref_range ?loc ptr len =
   let typ = ttype_of_pointed ptr.term_type in
   let range = tbuffer_range ?loc ptr len in
-  term (TLval ((TMem range), TNoOffset)) typ
+  let tlval = (TMem range), TNoOffset in
+  let tlval, typ = tunref_range_unfold ?loc tlval typ in
+  term (TLval tlval) typ
+and tunref_range_unfold ?loc lval typ =
+  match typ with
+  | Ctype(TArray(typ, Some e, _, _)) ->
+    let len = Logic_utils.expr_to_term ~cast:false e in
+    let last = tminus ?loc len (tinteger ?loc 1) in
+    let range = trange ?loc (Some (tinteger ?loc 0), Some last) in
+    let lval = addTermOffsetLval (TIndex(range, TNoOffset)) lval in
+    tunref_range_unfold lval (Ctype typ)
+  | _ -> lval, typ
+
+let taccess ?loc ptr offset =
+  let get_lval = function
+    | TLval(lval) -> lval
+    | _ -> assert false
+  in
+  match ptr.term_type with
+  | Ctype(TPtr(_)) ->
+    let address = tplus ?loc ptr offset in
+    let lval = TLval(TMem(address), TNoOffset) in
+    term ?loc lval (ttype_of_pointed ptr.term_type)
+  | Ctype(TArray(_)) ->
+    let lval = get_lval ptr.term_node in
+    let lval = addTermOffsetLval (TIndex(offset, TNoOffset)) lval in
+    term ?loc (TLval lval) (ttype_of_pointed ptr.term_type)
+  | _ -> assert false
 
 let tsizeofpointed ?loc = function
   | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> tinteger ?loc (Cil.bytesSizeOf t)
@@ -133,6 +161,29 @@ let pcorrect_len_bytes ?loc t bytes_len =
   let modulo = term ?loc (TBinOp(Mod, bytes_len, sizeof)) Linteger in
   prel ?loc (Req, modulo, tinteger ?loc 0)
 
+let pindex_bounds ?loc low value up =
+  let geq_0 = prel ?loc (Rle, low, value) in
+  let lt_len = prel ?loc (Rlt, value, up) in
+  pand ?loc (geq_0, lt_len)
+
+let rec punfold_all_elems_eq ?loc t1 t2 len =
+  assert(Cil_datatype.Logic_type.equal t1.term_type t2.term_type) ;
+  pall_elems_eq ?loc 0 t1 t2 len
+and pall_elems_eq ?loc depth t1 t2 len =
+  let ind = Cil_const.make_logic_var_quant ("j" ^ (string_of_int depth)) Linteger in
+  let tind = tvar ind in
+  let bounds = pindex_bounds ?loc (tinteger 0) tind len in
+  let t1_acc = taccess ?loc t1 tind in
+  let t2_acc = taccess ?loc t2 tind in
+  let eq = peq_unfold ?loc (depth+1) t1_acc t2_acc in
+  pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
+and peq_unfold ?loc depth t1 t2 =
+  match t1.term_type with
+  | Ctype(TArray(_, Some len, _, _)) ->
+    let len = Logic_utils.expr_to_term ~cast:false len in
+    pall_elems_eq ?loc depth t1 t2 len
+  | _ -> prel ?loc (Req, t1, t2)
+
 let pseparated_memories ?loc p1 len1 p2 len2 =
   let b1 = tbuffer_range ?loc p1 len1 in
   let b2 = tbuffer_range ?loc p2 len2 in
diff --git a/src/plugins/override_std/basic_blocks.mli b/src/plugins/override_std/basic_blocks.mli
index e2b0d5d0fffd7e52ec4dc36ca9509c5550f7642e..7ece0de7ecc1bd00c9f3c535dbb3cf99d6643dee 100644
--- a/src/plugins/override_std/basic_blocks.mli
+++ b/src/plugins/override_std/basic_blocks.mli
@@ -40,6 +40,7 @@ val tdivide: ?loc:location -> term -> term -> term
 val pvalid_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
 val pvalid_read_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
 val pcorrect_len_bytes: ?loc:location -> logic_type -> term -> predicate
+val punfold_all_elems_eq: ?loc:location -> term -> term -> term -> predicate
 
 val pseparated_memories: ?loc:location -> term -> term -> term -> term -> predicate
 
diff --git a/src/plugins/override_std/memcmp.ml b/src/plugins/override_std/memcmp.ml
index 39ede274dbb98df882ba8c9a45a11f7f34841c7e..f1d6bfeff5603b7010d1cd5f7d00a42cd0f7a554 100644
--- a/src/plugins/override_std/memcmp.ml
+++ b/src/plugins/override_std/memcmp.ml
@@ -34,18 +34,9 @@ let generate_requires loc s1 s2 len =
   ]
 
 let presult_memcmp ?loc p1 p2 len =
-  let j = Cil_const.make_logic_var_quant "j" Linteger in
-  let tj = tvar j in
-  let geq_0 = prel ?loc (Rle, (tinteger 0), tj) in
-  let lt_len = prel ?loc (Rlt, tj, len) in
-  let bounds = pand ?loc (geq_0, lt_len) in
-  let p1_j = tplus ?loc p1 tj in
-  let p1_acc = term ?loc (TLval(TMem(p1_j), TNoOffset)) (ttype_of_pointed p1.term_type) in
-  let p2_j = tplus ?loc p2 tj in
-  let p2_acc = term ?loc (TLval(TMem(p2_j), TNoOffset)) (ttype_of_pointed p2.term_type) in
-  let eq = prel ?loc (Req, p1_acc, p2_acc) in
+  let eq = punfold_all_elems_eq ?loc p1 p2 len in
   let res = prel ?loc (Req, (tresult ?loc Cil.intType), (tinteger ?loc 0)) in
-  piff ?loc (res, pforall ?loc ([j], (pimplies ?loc (bounds, eq))))
+  piff ?loc (res, eq)
 
 let generate_assigns loc t s1 s2 len =
   let indirect_range loc s len =
diff --git a/src/plugins/override_std/memcpy.ml b/src/plugins/override_std/memcpy.ml
index f3a789cb2e7a2b5feef5e0f06361d5ba7f624770..beae7eb2bd08d56ff639a7d292359185bb429fc7 100644
--- a/src/plugins/override_std/memcpy.ml
+++ b/src/plugins/override_std/memcpy.ml
@@ -30,21 +30,8 @@ let pseparated_memcpy_len_bytes ?loc p1 p2 bytes_len =
   let generate len = pseparated_memories ?loc p1 len p2 len in
   plet_len_div_size ?loc p1.term_type bytes_len generate
 
-let pcopied_memcpy ?loc p1 p2 len =
-  let j = Cil_const.make_logic_var_quant "j" Linteger in
-  let tj = tvar j in
-  let geq_0 = prel ?loc (Rle, (tinteger 0), tj) in
-  let lt_len = prel ?loc (Rlt, tj, len) in
-  let bounds = pand ?loc (geq_0, lt_len) in
-  let p1_j = tplus ?loc p1 tj in
-  let p1_acc = term ?loc (TLval(TMem(p1_j), TNoOffset)) (ttype_of_pointed p1.term_type) in
-  let p2_j = tplus ?loc p2 tj in
-  let p2_acc = term ?loc (TLval(TMem(p2_j), TNoOffset)) (ttype_of_pointed p2.term_type) in
-  let eq = prel ?loc (Req, p1_acc, p2_acc) in
-  pforall ?loc ([j], (pimplies ?loc (bounds, eq)))
-
 let pcopied_len_bytes ?loc p1 p2 bytes_len =
-  plet_len_div_size ?loc p1.term_type bytes_len (pcopied_memcpy ?loc p1 p2)
+  plet_len_div_size ?loc p1.term_type bytes_len (punfold_all_elems_eq ?loc p1 p2)
 
 let presult_dest ?loc t dest =
   prel ?loc (Req, (tresult ?loc t), dest)
diff --git a/src/plugins/override_std/memmove.ml b/src/plugins/override_std/memmove.ml
index a29ca3383e5b613cb2d6b5b5d93925a3be2613ec..cd292e512a9d8ce6b3ba8beb1d7a0bcab9fb5d6c 100644
--- a/src/plugins/override_std/memmove.ml
+++ b/src/plugins/override_std/memmove.ml
@@ -26,22 +26,8 @@ open Basic_blocks
 
 let function_name = "memmove"
 
-let pmoved_memmove ?loc dest src len =
-  let j = Cil_const.make_logic_var_quant "j" Linteger in
-  let tj = tvar j in
-  let geq_0 = prel ?loc (Rle, (tinteger 0), tj) in
-  let lt_len = prel ?loc (Rlt, tj, len) in
-  let bounds = pand ?loc (geq_0, lt_len) in
-  let dest_j = tplus ?loc dest tj in
-  let dest_acc = term ?loc (TLval(TMem(dest_j), TNoOffset)) (ttype_of_pointed dest.term_type) in
-  let src_j = tplus ?loc src tj in
-  let src_acc = term ?loc (TLval(TMem(src_j), TNoOffset)) (ttype_of_pointed dest.term_type) in
-  let src_acc = tat ?loc (src_acc, pre_label) in
-  let eq = prel ?loc (Req, dest_acc, src_acc) in
-  pforall ?loc ([j], (pimplies ?loc (bounds, eq)))
-
 let pmoved_len_bytes ?loc dest src bytes_len =
-  plet_len_div_size ?loc dest.term_type bytes_len (pmoved_memmove ?loc dest src)
+  plet_len_div_size ?loc dest.term_type bytes_len (punfold_all_elems_eq ?loc dest src)
 
 let presult_dest ?loc t dest =
   prel ?loc (Req, (tresult ?loc t), dest)
diff --git a/src/plugins/override_std/tests/functions/memcmp.c b/src/plugins/override_std/tests/functions/memcmp.c
index 1da39df89a53462b2d9767208cebbd72b44acca0..67d1b22a5791938c04d29ecc324faf1b87fc43e6 100644
--- a/src/plugins/override_std/tests/functions/memcmp.c
+++ b/src/plugins/override_std/tests/functions/memcmp.c
@@ -5,4 +5,8 @@ int main(void){
   int s2[10] = { 0 };
 
   int res = memcmp(s1, s2, sizeof(s1));
+}
+
+int nested(int (*dest) [10], int (*src) [10], size_t n){
+  return memcmp(dest, src, n) ;
 }
\ No newline at end of file
diff --git a/src/plugins/override_std/tests/functions/memcpy.c b/src/plugins/override_std/tests/functions/memcpy.c
index 7dda713ac6d1c8212fb18bce80edd245e16bace3..7264434129d5ddb64a262ff5e0f6a231f5d6f842 100644
--- a/src/plugins/override_std/tests/functions/memcpy.c
+++ b/src/plugins/override_std/tests/functions/memcpy.c
@@ -5,4 +5,8 @@ int main(void){
   int dest[10] ;
 
   int *p = memcpy(dest, src, sizeof(src));
+}
+
+void nested(int (*dest) [10], int (*src) [10], size_t n){
+  memcpy(dest, src, n) ;
 }
\ No newline at end of file
diff --git a/src/plugins/override_std/tests/functions/memmove.c b/src/plugins/override_std/tests/functions/memmove.c
index 33338d2d312753e8b519e16aa7657765da2d7f64..d97eda5defe9355cb1c26465802bb516bf00b390 100644
--- a/src/plugins/override_std/tests/functions/memmove.c
+++ b/src/plugins/override_std/tests/functions/memmove.c
@@ -5,4 +5,8 @@ int main(void){
   int dest[10] ;
 
   int *p = memmove(dest, src, sizeof(src));
+}
+
+int* nested(int (*dest) [10], int (*src) [10], size_t n){
+  memmove(dest, src, n) ;
 }
\ No newline at end of file
diff --git a/src/plugins/override_std/tests/functions/oracle/memcmp.res.oracle b/src/plugins/override_std/tests/functions/oracle/memcmp.res.oracle
index 7ece1fdb38954432441e08ccc48f8a48cabbc28c..456152c88ffcb8729e542012f021dab3cefe3e55 100644
--- a/src/plugins/override_std/tests/functions/oracle/memcmp.res.oracle
+++ b/src/plugins/override_std/tests/functions/oracle/memcmp.res.oracle
@@ -3,6 +3,28 @@
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+/*@ requires aligned_end: len % 40 ≡ 0;
+    requires
+      valid_read_s1:
+        \let __fc_len = len / 40; \valid_read(s1 + (0 .. __fc_len - 1));
+    requires
+      valid_read_s2:
+        \let __fc_len = len / 40; \valid_read(s2 + (0 .. __fc_len - 1));
+    ensures
+      equals:
+        \let __fc_len = len / 40;
+          \result ≡ 0 ⇔
+          (∀ ℤ j0;
+             0 ≤ j0 < __fc_len ⇒
+             (∀ ℤ j1;
+                0 ≤ j1 < 10 ⇒ (*(s1 + j0))[j1] ≡ (*(s2 + j0))[j1]));
+    assigns \result;
+    assigns \result
+      \from (indirect: (*(s1 + (0 .. len - 1)))[0 .. 10 - 1]),
+            (indirect: (*(s2 + (0 .. len - 1)))[0 .. 10 - 1]);
+ */
+int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len);
+
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_read_s1:
@@ -14,7 +36,7 @@
       equals:
         \let __fc_len = len / 4;
           \result ≡ 0 ⇔
-          (∀ ℤ j; 0 ≤ j < __fc_len ⇒ *(s1 + j) ≡ *(s2 + j));
+          (∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
     assigns \result;
     assigns \result
       \from (indirect: *(s1 + (0 .. len - 1))),
@@ -32,15 +54,47 @@ int main(void)
   return __retres;
 }
 
+int nested(int (*dest)[10], int (*src)[10], size_t n)
+{
+  int tmp;
+  tmp = memcmp_arr10_int(dest,src,n);
+  return tmp;
+}
+
 
 [kernel] Parsing tests/functions/result/memcmp.c (with preprocessing)
 [kernel] Parsing tests/functions/memcmp.c (with preprocessing)
 [kernel] tests/functions/memcmp.c:3: Warning: 
-  def'n of func main at tests/functions/memcmp.c:3 (sum 2855) conflicts with the one at tests/functions/result/memcmp.c:24 (sum 4629); keeping the one at tests/functions/result/memcmp.c:24.
+  def'n of func main at tests/functions/memcmp.c:3 (sum 2855) conflicts with the one at tests/functions/result/memcmp.c:46 (sum 4629); keeping the one at tests/functions/result/memcmp.c:46.
+[kernel] tests/functions/memcmp.c:10: Warning: 
+  def'n of func nested at tests/functions/memcmp.c:10 (sum 1087) conflicts with the one at tests/functions/result/memcmp.c:56 (sum 1974); keeping the one at tests/functions/result/memcmp.c:56.
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+/*@ requires aligned_end: len % 40 ≡ 0;
+    requires
+      valid_read_s1:
+        \let __fc_len = len / 40; \valid_read(s1 + (0 .. __fc_len - 1));
+    requires
+      valid_read_s2:
+        \let __fc_len = len / 40; \valid_read(s2 + (0 .. __fc_len - 1));
+    ensures
+      equals:
+        \let __fc_len = \old(len) / 40;
+          \result ≡ 0 ⇔
+          (∀ ℤ j0;
+             0 ≤ j0 < __fc_len ⇒
+             (∀ ℤ j1;
+                0 ≤ j1 < 10 ⇒
+                (*(\old(s1) + j0))[j1] ≡ (*(\old(s2) + j0))[j1]));
+    assigns \result;
+    assigns \result
+      \from (indirect: (*(s1 + (0 .. len - 1)))[0 .. 10 - 1]),
+            (indirect: (*(s2 + (0 .. len - 1)))[0 .. 10 - 1]);
+ */
+int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len);
+
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_read_s1:
@@ -52,8 +106,8 @@ int main(void)
       equals:
         \let __fc_len = \old(len) / 4;
           \result ≡ 0 ⇔
-          (∀ ℤ j;
-             0 ≤ j < __fc_len ⇒ *(\old(s1) + j) ≡ *(\old(s2) + j));
+          (∀ ℤ j0;
+             0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0));
     assigns \result;
     assigns \result
       \from (indirect: *(s1 + (0 .. len - 1))),
@@ -71,4 +125,11 @@ int main(void)
   return __retres;
 }
 
+int nested(int (*dest)[10], int (*src)[10], size_t n)
+{
+  int tmp;
+  tmp = memcmp_arr10_int((int const (*)[10])dest,(int const (*)[10])src,n);
+  return tmp;
+}
+
 
diff --git a/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle b/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle
index 6bb3d9d1bb5f9c028c073d1aed1e3546b0130efa..86774bd9c828f562828d6b2b63a9e40e1385daa8 100644
--- a/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle
+++ b/src/plugins/override_std/tests/functions/oracle/memcpy.res.oracle
@@ -3,6 +3,32 @@
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+/*@ requires aligned_end: len % 40 ≡ 0;
+    requires
+      valid_dest:
+        \let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
+    requires
+      separation:
+        \let __fc_len = len / 40;
+          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+    ensures
+      copied:
+        \let __fc_len = len / 40;
+        ∀ ℤ j0;
+          0 ≤ j0 < __fc_len ⇒
+          (∀ ℤ j1;
+             0 ≤ j1 < 10 ⇒ (*(dest + j0))[j1] ≡ (*(src + j0))[j1]);
+    ensures result: \result ≡ dest;
+    assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
+    assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
+      \from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
+    assigns \result \from dest;
+ */
+int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
+
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -16,7 +42,7 @@
     ensures
       copied:
         \let __fc_len = len / 4;
-        ∀ ℤ j; 0 ≤ j < __fc_len ⇒ *(dest + j) ≡ *(src + j);
+        ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
     ensures result: \result ≡ dest;
     assigns *(dest + (0 .. len - 1)), \result;
     assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
@@ -34,15 +60,50 @@ int main(void)
   return __retres;
 }
 
+void nested(int (*dest)[10], int (*src)[10], size_t n)
+{
+  memcpy_arr10_int(dest,src,n);
+  return;
+}
+
 
 [kernel] Parsing tests/functions/result/memcpy.c (with preprocessing)
 [kernel] Parsing tests/functions/memcpy.c (with preprocessing)
 [kernel] tests/functions/memcpy.c:3: Warning: 
-  def'n of func main at tests/functions/memcpy.c:3 (sum 1968) conflicts with the one at tests/functions/result/memcpy.c:26 (sum 3742); keeping the one at tests/functions/result/memcpy.c:26.
+  def'n of func main at tests/functions/memcpy.c:3 (sum 1968) conflicts with the one at tests/functions/result/memcpy.c:52 (sum 3742); keeping the one at tests/functions/result/memcpy.c:52.
+[kernel] tests/functions/memcpy.c:10: Warning: 
+  dropping duplicate def'n of func nested at tests/functions/memcpy.c:10 in favor of that at tests/functions/result/memcpy.c:62
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+/*@ requires aligned_end: len % 40 ≡ 0;
+    requires
+      valid_dest:
+        \let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
+    requires
+      separation:
+        \let __fc_len = len / 40;
+          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+    ensures
+      copied:
+        \let __fc_len = \old(len) / 40;
+        ∀ ℤ j0;
+          0 ≤ j0 < __fc_len ⇒
+          (∀ ℤ j1;
+             0 ≤ j1 < 10 ⇒
+             (*(\old(dest) + j0))[j1] ≡ (*(\old(src) + j0))[j1]);
+    ensures result: \result ≡ \old(dest);
+    assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
+    assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
+      \from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
+    assigns \result \from dest;
+ */
+int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
+
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -56,8 +117,8 @@ int main(void)
     ensures
       copied:
         \let __fc_len = \old(len) / 4;
-        ∀ ℤ j;
-          0 ≤ j < __fc_len ⇒ *(\old(dest) + j) ≡ *(\old(src) + j);
+        ∀ ℤ j0;
+          0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
     ensures result: \result ≡ \old(dest);
     assigns *(dest + (0 .. len - 1)), \result;
     assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
@@ -75,4 +136,10 @@ int main(void)
   return __retres;
 }
 
+void nested(int (*dest)[10], int (*src)[10], size_t n)
+{
+  memcpy_arr10_int(dest,(int const (*)[10])src,n);
+  return;
+}
+
 
diff --git a/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle b/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle
index 2db11ab0c0c9b2d701909ab870afad5cbe18cb77..314166b974d82d8bb41ec4fc3cd5235d8e0178be 100644
--- a/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle
+++ b/src/plugins/override_std/tests/functions/oracle/memmove.res.oracle
@@ -1,8 +1,32 @@
 [kernel] Parsing tests/functions/memmove.c (with preprocessing)
+[kernel] tests/functions/memmove.c:11: Warning: 
+  Body of function nested falls-through. Adding a return statement
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+/*@ requires aligned_end: len % 40 ≡ 0;
+    requires
+      valid_dest:
+        \let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
+    ensures
+      moved:
+        \let __fc_len = len / 40;
+        ∀ ℤ j0;
+          0 ≤ j0 < __fc_len ⇒
+          (∀ ℤ j1;
+             0 ≤ j1 < 10 ⇒ (*(dest + j0))[j1] ≡ (*(src + j0))[j1]);
+    ensures result: \result ≡ dest;
+    assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
+    assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
+      \from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
+    assigns \result \from dest;
+ */
+int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
+
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -12,7 +36,7 @@
     ensures
       moved:
         \let __fc_len = len / 4;
-        ∀ ℤ j; 0 ≤ j < __fc_len ⇒ *(dest + j) ≡ \at(*(src + j),Pre);
+        ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
     ensures result: \result ≡ dest;
     assigns *(dest + (0 .. len - 1)), \result;
     assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
@@ -30,15 +54,51 @@ int main(void)
   return __retres;
 }
 
+int *nested(int (*dest)[10], int (*src)[10], size_t n)
+{
+  int *__retres;
+  memmove_arr10_int(dest,src,n);
+  /*@ assert missing_return: \false; */ ;
+  __retres = (int *)0;
+  return __retres;
+}
+
 
 [kernel] Parsing tests/functions/result/memmove.c (with preprocessing)
 [kernel] Parsing tests/functions/memmove.c (with preprocessing)
+[kernel] tests/functions/memmove.c:11: Warning: 
+  Body of function nested falls-through. Adding a return statement
 [kernel] tests/functions/memmove.c:3: Warning: 
-  def'n of func main at tests/functions/memmove.c:3 (sum 1968) conflicts with the one at tests/functions/result/memmove.c:22 (sum 3742); keeping the one at tests/functions/result/memmove.c:22.
+  def'n of func main at tests/functions/memmove.c:3 (sum 1968) conflicts with the one at tests/functions/result/memmove.c:44 (sum 3742); keeping the one at tests/functions/result/memmove.c:44.
+[kernel] tests/functions/memmove.c:10: Warning: 
+  def'n of func nested at tests/functions/memmove.c:10 (sum 1974) conflicts with the one at tests/functions/result/memmove.c:54 (sum 4635); keeping the one at tests/functions/result/memmove.c:54.
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+/*@ requires aligned_end: len % 40 ≡ 0;
+    requires
+      valid_dest:
+        \let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
+    ensures
+      moved:
+        \let __fc_len = \old(len) / 40;
+        ∀ ℤ j0;
+          0 ≤ j0 < __fc_len ⇒
+          (∀ ℤ j1;
+             0 ≤ j1 < 10 ⇒
+             (*(\old(dest) + j0))[j1] ≡ (*(\old(src) + j0))[j1]);
+    ensures result: \result ≡ \old(dest);
+    assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
+    assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
+      \from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
+    assigns \result \from dest;
+ */
+int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
+
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -48,8 +108,8 @@ int main(void)
     ensures
       moved:
         \let __fc_len = \old(len) / 4;
-        ∀ ℤ j;
-          0 ≤ j < __fc_len ⇒ *(\old(dest) + j) ≡ \at(*(src + j),Pre);
+        ∀ ℤ j0;
+          0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
     ensures result: \result ≡ \old(dest);
     assigns *(dest + (0 .. len - 1)), \result;
     assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
@@ -67,4 +127,13 @@ int main(void)
   return __retres;
 }
 
+int *nested(int (*dest)[10], int (*src)[10], size_t n)
+{
+  int *__retres;
+  memmove_arr10_int(dest,(int const (*)[10])src,n);
+  /*@ assert missing_return: \false; */ ;
+  __retres = (int *)0;
+  return __retres;
+}
+