diff --git a/src/plugins/builtin/tests/functions/memcmp.c b/src/plugins/builtin/tests/functions/memcmp.c
index 67d1b22a5791938c04d29ecc324faf1b87fc43e6..8a0b48622a604a70d577c4c8d85abe847214e98e 100644
--- a/src/plugins/builtin/tests/functions/memcmp.c
+++ b/src/plugins/builtin/tests/functions/memcmp.c
@@ -1,12 +1,28 @@
 #include <string.h>
 
-int main(void){
-  int s1[10] = { 0 } ;
-  int s2[10] = { 0 };
+struct X {
+  int x ;
+  int y ;
+} ;
 
-  int res = memcmp(s1, s2, sizeof(s1));
+typedef int named ;
+
+int integer(int src[10], int dest[10]){
+  return memcmp(dest, src, 10 * sizeof(int));
+}
+
+int with_named(named src[10], named dest[10]){
+  return memcmp(dest, src, 10 * sizeof(named));
+}
+
+int structure(struct X src[10], struct X dest[10]){
+  return memcmp(dest, src, 10 * sizeof(struct X));
+}
+
+int pointers(int* src[10], int* dest[10]){
+  return memcmp(dest, src, 10 * sizeof(int*));
 }
 
-int nested(int (*dest) [10], int (*src) [10], size_t n){
-  return memcmp(dest, src, n) ;
-}
\ No newline at end of file
+int nested(int (*src)[10], int (*dest)[10], int n){
+  return memcmp(dest, src, n * sizeof(int[10]));
+}
diff --git a/src/plugins/builtin/tests/functions/memcpy.c b/src/plugins/builtin/tests/functions/memcpy.c
index 7264434129d5ddb64a262ff5e0f6a231f5d6f842..ed3022f37184cd9cb47a4029525c9407e2040348 100644
--- a/src/plugins/builtin/tests/functions/memcpy.c
+++ b/src/plugins/builtin/tests/functions/memcpy.c
@@ -1,12 +1,33 @@
 #include <string.h>
 
-int main(void){
-  int src[10] = { 0 } ;
-  int dest[10] ;
+struct X {
+  int x ;
+  int y ;
+} ;
 
-  int *p = memcpy(dest, src, sizeof(src));
+typedef int named ;
+
+void integer(int src[10], int dest[10]){
+  int * res = memcpy(dest, src, 10 * sizeof(int));
+  memcpy(src, res, 10 * sizeof(int));
+}
+
+void with_named(named src[10], named dest[10]){
+  named * res = memcpy(dest, src, 10 * sizeof(named));
+  memcpy(src, res, 10 * sizeof(named));
+}
+
+void structure(struct X src[10], struct X dest[10]){
+  struct X * res = memcpy(dest, src, 10 * sizeof(struct X));
+  memcpy(src, res, 10 * sizeof(struct X));
+}
+
+void pointers(int* src[10], int* dest[10]){
+  int ** res = memcpy(dest, src, 10 * sizeof(int*));
+  memcpy(src, res, 10 * sizeof(int*));
 }
 
-void nested(int (*dest) [10], int (*src) [10], size_t n){
-  memcpy(dest, src, n) ;
-}
\ No newline at end of file
+void nested(int (*src)[10], int (*dest)[10], int n){
+  int (*res) [10] = memcpy(dest, src, n * sizeof(int[10]));
+  memcpy(src, res, n * sizeof(int[10]));
+}
diff --git a/src/plugins/builtin/tests/functions/memmove.c b/src/plugins/builtin/tests/functions/memmove.c
index 7a17026266d3fe21d3af5411715e868baa97c7c1..3944ba0356393d9c72b479a4e4cdc29011027d40 100644
--- a/src/plugins/builtin/tests/functions/memmove.c
+++ b/src/plugins/builtin/tests/functions/memmove.c
@@ -1,12 +1,33 @@
 #include <string.h>
 
-int main(void){
-  int src[10] = { 0 } ;
-  int dest[10] ;
+struct X {
+  int x ;
+  int y ;
+} ;
 
-  int *p = memmove(dest, src, sizeof(src));
+typedef int named ;
+
+void integer(int src[10], int dest[10]){
+  int * res = memmove(dest, src, 10 * sizeof(int));
+  memmove(src, res, 10 * sizeof(int));
+}
+
+void with_named(named src[10], named dest[10]){
+  named * res = memmove(dest, src, 10 * sizeof(named));
+  memmove(src, res, 10 * sizeof(named));
+}
+
+void structure(struct X src[10], struct X dest[10]){
+  struct X * res = memmove(dest, src, 10 * sizeof(struct X));
+  memmove(src, res, 10 * sizeof(struct X));
+}
+
+void pointers(int* src[10], int* dest[10]){
+  int ** res = memmove(dest, src, 10 * sizeof(int*));
+  memmove(src, res, 10 * sizeof(int*));
 }
 
-void nested(int (*dest) [10], int (*src) [10], size_t n) {
-  memmove(dest, src, n) ;
-}
\ No newline at end of file
+void nested(int (*src)[10], int (*dest)[10], int n){
+  int (*res) [10] = memmove(dest, src, n * sizeof(int[10]));
+  memmove(src, res, n * sizeof(int[10]));
+}
diff --git a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle b/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
index 77e86fe5a03fe77a5a9665dd6784e0bf69e3b447..b0d88d0280a155addeb1e1fb960868b71896202d 100644
--- a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
@@ -3,6 +3,11 @@
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+struct X {
+   int x ;
+   int y ;
+};
+typedef int named;
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_read_s1:
@@ -27,16 +32,82 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
   return __retres;
 }
 
-int main(void)
+int integer(int * /*[10]*/ src, int * /*[10]*/ dest)
+{
+  int tmp;
+  tmp = memcmp_int(dest,src,(unsigned int)10 * sizeof(int));
+  return tmp;
+}
+
+int with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
+{
+  int tmp;
+  tmp = memcmp_int(dest,src,(unsigned int)10 * sizeof(named));
+  return tmp;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+    requires
+      valid_read_s1:
+        \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
+    requires
+      valid_read_s2:
+        \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
+    ensures
+      equals:
+        \let __fc_len = len / 8;
+          \result ≡ 0 ⇔
+          (∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
+    assigns \result;
+    assigns \result
+      \from (indirect: *(s1 + (0 .. len - 1))),
+            (indirect: *(s2 + (0 .. len - 1)));
+ */
+int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
+{
+  int __retres;
+  __retres = memcmp((void const *)s1,(void const *)s2,len);
+  return __retres;
+}
+
+int structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
+{
+  int tmp;
+  tmp = memcmp_X(dest,src,(unsigned int)10 * sizeof(struct X));
+  return tmp;
+}
+
+/*@ requires aligned_end: len % 4 ≡ 0;
+    requires
+      valid_read_s1:
+        \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1));
+    requires
+      valid_read_s2:
+        \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1));
+    ensures
+      equals:
+        \let __fc_len = len / 4;
+          \result ≡ 0 ⇔
+          (∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
+    assigns \result;
+    assigns \result
+      \from (indirect: *(s1 + (0 .. len - 1))),
+            (indirect: *(s2 + (0 .. len - 1)));
+ */
+int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
 {
   int __retres;
-  int s1[10] = {0};
-  int s2[10] = {0};
-  int res = memcmp_int(s1,s2,sizeof(s1));
-  __retres = 0;
+  __retres = memcmp((void const *)s1,(void const *)s2,len);
   return __retres;
 }
 
+int pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
+{
+  int tmp;
+  tmp = memcmp_ptr_int(dest,src,(unsigned int)10 * sizeof(int *));
+  return tmp;
+}
+
 /*@ requires aligned_end: len % 40 ≡ 0;
     requires
       valid_read_s1:
@@ -64,24 +135,35 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
   return __retres;
 }
 
-int nested(int (*dest)[10], int (*src)[10], size_t n)
+int nested(int (*src)[10], int (*dest)[10], int n)
 {
   int tmp;
-  tmp = memcmp_arr10_int(dest,src,n);
+  tmp = memcmp_arr10_int(dest,src,(unsigned int)n * sizeof(int [10]));
   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:29 (sum 4629); keeping the one at tests/functions/result/memcmp.c:29.
 [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:66 (sum 1974); keeping the one at tests/functions/result/memcmp.c:66.
+  def'n of func integer at tests/functions/memcmp.c:10 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:34 (sum 1972); keeping the one at tests/functions/result/memcmp.c:34.
+[kernel] tests/functions/memcmp.c:14: Warning: 
+  def'n of func with_named at tests/functions/memcmp.c:14 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:41 (sum 1972); keeping the one at tests/functions/result/memcmp.c:41.
+[kernel] tests/functions/memcmp.c:18: Warning: 
+  def'n of func structure at tests/functions/memcmp.c:18 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:72 (sum 1972); keeping the one at tests/functions/result/memcmp.c:72.
+[kernel] tests/functions/memcmp.c:22: Warning: 
+  def'n of func pointers at tests/functions/memcmp.c:22 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:103 (sum 1972); keeping the one at tests/functions/result/memcmp.c:103.
+[kernel] tests/functions/memcmp.c:26: Warning: 
+  def'n of func nested at tests/functions/memcmp.c:26 (sum 1087) conflicts with the one at tests/functions/result/memcmp.c:137 (sum 1974); keeping the one at tests/functions/result/memcmp.c:137.
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+struct X {
+   int x ;
+   int y ;
+};
+typedef int named;
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_read_s1:
@@ -107,16 +189,88 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
   return __retres;
 }
 
-int main(void)
+int integer(int *src, int *dest)
+{
+  int tmp;
+  tmp = memcmp_int((int const *)dest,(int const *)src,
+                   (unsigned int)10 * sizeof(int));
+  return tmp;
+}
+
+int with_named(named *src, named *dest)
+{
+  int tmp;
+  tmp = memcmp_int((int const *)dest,(int const *)src,
+                   (unsigned int)10 * sizeof(named));
+  return tmp;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+    requires
+      valid_read_s1:
+        \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
+    requires
+      valid_read_s2:
+        \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
+    ensures
+      equals:
+        \let __fc_len = \old(len) / 8;
+          \result ≡ 0 ⇔
+          (∀ ℤ j0;
+             0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0));
+    assigns \result;
+    assigns \result
+      \from (indirect: *(s1 + (0 .. len - 1))),
+            (indirect: *(s2 + (0 .. len - 1)));
+ */
+int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
+{
+  int __retres;
+  __retres = memcmp((void const *)s1,(void const *)s2,len);
+  return __retres;
+}
+
+int structure(struct X *src, struct X *dest)
+{
+  int tmp;
+  tmp = memcmp_X((struct X const *)dest,(struct X const *)src,
+                 (unsigned int)10 * sizeof(struct X));
+  return tmp;
+}
+
+/*@ requires aligned_end: len % 4 ≡ 0;
+    requires
+      valid_read_s1:
+        \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1));
+    requires
+      valid_read_s2:
+        \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1));
+    ensures
+      equals:
+        \let __fc_len = \old(len) / 4;
+          \result ≡ 0 ⇔
+          (∀ ℤ j0;
+             0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0));
+    assigns \result;
+    assigns \result
+      \from (indirect: *(s1 + (0 .. len - 1))),
+            (indirect: *(s2 + (0 .. len - 1)));
+ */
+int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
 {
   int __retres;
-  int s1[10] = {0};
-  int s2[10] = {0};
-  int res = memcmp_int((int const *)(s1),(int const *)(s2),sizeof(s1));
-  __retres = 0;
+  __retres = memcmp((void const *)s1,(void const *)s2,len);
   return __retres;
 }
 
+int pointers(int **src, int **dest)
+{
+  int tmp;
+  tmp = memcmp_ptr_int((int * const *)dest,(int * const *)src,
+                       (unsigned int)10 * sizeof(int *));
+  return tmp;
+}
+
 /*@ requires aligned_end: len % 40 ≡ 0;
     requires
       valid_read_s1:
@@ -145,10 +299,11 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
   return __retres;
 }
 
-int nested(int (*dest)[10], int (*src)[10], size_t n)
+int nested(int (*src)[10], int (*dest)[10], int n)
 {
   int tmp;
-  tmp = memcmp_arr10_int((int const (*)[10])dest,(int const (*)[10])src,n);
+  tmp = memcmp_arr10_int((int const (*)[10])dest,(int const (*)[10])src,
+                         (unsigned int)n * sizeof(int [10]));
   return tmp;
 }
 
diff --git a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle b/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
index 7c8012b7448858d598c0bab558ad7559c994f605..b29798e2515dc29fe898a22bc591785a030c417c 100644
--- a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
@@ -3,6 +3,11 @@
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+struct X {
+   int x ;
+   int y ;
+};
+typedef int named;
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -29,16 +34,86 @@ int *memcpy_int(int *dest, int const *src, size_t len)
   return __retres;
 }
 
-int main(void)
+void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
 {
-  int __retres;
-  int dest[10];
-  int src[10] = {0};
-  int *p = memcpy_int(dest,src,sizeof(src));
-  __retres = 0;
+  int *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(int));
+  memcpy_int(src,res,(unsigned int)10 * sizeof(int));
+  return;
+}
+
+void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
+{
+  named *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(named));
+  memcpy_int(src,res,(unsigned int)10 * sizeof(named));
+  return;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+    requires
+      valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
+    requires
+      separation:
+        \let __fc_len = len / 8;
+          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+    ensures
+      copied:
+        \let __fc_len = len / 8;
+        ∀ ℤ 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));
+    assigns \result \from dest;
+ */
+struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
+{
+  struct X *__retres;
+  __retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
+  return __retres;
+}
+
+void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
+{
+  struct X *res = memcpy_X(dest,src,(unsigned int)10 * sizeof(struct X));
+  memcpy_X(src,res,(unsigned int)10 * sizeof(struct X));
+  return;
+}
+
+/*@ requires aligned_end: len % 4 ≡ 0;
+    requires
+      valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+    requires
+      separation:
+        \let __fc_len = len / 4;
+          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+    ensures
+      copied:
+        \let __fc_len = len / 4;
+        ∀ ℤ 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));
+    assigns \result \from dest;
+ */
+int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
+{
+  int **__retres;
+  __retres = (int **)memcpy((void *)dest,(void const *)src,len);
   return __retres;
 }
 
+void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
+{
+  int **res = memcpy_ptr_int(dest,src,(unsigned int)10 * sizeof(int *));
+  memcpy_ptr_int(src,res,(unsigned int)10 * sizeof(int *));
+  return;
+}
+
 /*@ requires aligned_end: len % 40 ≡ 0;
     requires
       valid_dest:
@@ -70,23 +145,36 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
   return __retres;
 }
 
-void nested(int (*dest)[10], int (*src)[10], size_t n)
+void nested(int (*src)[10], int (*dest)[10], int n)
 {
-  memcpy_arr10_int(dest,src,n);
+  int (*res)[10] =
+    memcpy_arr10_int(dest,src,(unsigned int)n * sizeof(int [10]));
+  memcpy_arr10_int(src,res,(unsigned int)n * sizeof(int [10]));
   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:31 (sum 3742); keeping the one at tests/functions/result/memcpy.c:31.
 [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:72
+  dropping duplicate def'n of func integer at tests/functions/memcpy.c:10 in favor of that at tests/functions/result/memcpy.c:36
+[kernel] tests/functions/memcpy.c:15: Warning: 
+  dropping duplicate def'n of func with_named at tests/functions/memcpy.c:15 in favor of that at tests/functions/result/memcpy.c:43
+[kernel] tests/functions/memcpy.c:20: Warning: 
+  dropping duplicate def'n of func structure at tests/functions/memcpy.c:20 in favor of that at tests/functions/result/memcpy.c:76
+[kernel] tests/functions/memcpy.c:25: Warning: 
+  dropping duplicate def'n of func pointers at tests/functions/memcpy.c:25 in favor of that at tests/functions/result/memcpy.c:109
+[kernel] tests/functions/memcpy.c:30: Warning: 
+  dropping duplicate def'n of func nested at tests/functions/memcpy.c:30 in favor of that at tests/functions/result/memcpy.c:147
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+struct X {
+   int x ;
+   int y ;
+};
+typedef int named;
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -114,16 +202,92 @@ int *memcpy_int(int *dest, int const *src, size_t len)
   return __retres;
 }
 
-int main(void)
+void integer(int *src, int *dest)
+{
+  int *res =
+    memcpy_int(dest,(int const *)src,(unsigned int)10 * sizeof(int));
+  memcpy_int(src,(int const *)res,(unsigned int)10 * sizeof(int));
+  return;
+}
+
+void with_named(named *src, named *dest)
+{
+  named *res =
+    memcpy_int(dest,(int const *)src,(unsigned int)10 * sizeof(named));
+  memcpy_int(src,(int const *)res,(unsigned int)10 * sizeof(named));
+  return;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+    requires
+      valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
+    requires
+      separation:
+        \let __fc_len = len / 8;
+          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+    ensures
+      copied:
+        \let __fc_len = \old(len) / 8;
+        ∀ ℤ 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));
+    assigns \result \from dest;
+ */
+struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
+{
+  struct X *__retres;
+  __retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
+  return __retres;
+}
+
+void structure(struct X *src, struct X *dest)
+{
+  struct X *res =
+    memcpy_X(dest,(struct X const *)src,(unsigned int)10 * sizeof(struct X));
+  memcpy_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+  return;
+}
+
+/*@ requires aligned_end: len % 4 ≡ 0;
+    requires
+      valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+    requires
+      separation:
+        \let __fc_len = len / 4;
+          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+    ensures
+      copied:
+        \let __fc_len = \old(len) / 4;
+        ∀ ℤ 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));
+    assigns \result \from dest;
+ */
+int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
 {
-  int __retres;
-  int dest[10];
-  int src[10] = {0};
-  int *p = memcpy_int(dest,(int const *)(src),sizeof(src));
-  __retres = 0;
+  int **__retres;
+  __retres = (int **)memcpy((void *)dest,(void const *)src,len);
   return __retres;
 }
 
+void pointers(int **src, int **dest)
+{
+  int **res =
+    memcpy_ptr_int(dest,(int * const *)src,(unsigned int)10 * sizeof(int *));
+  memcpy_ptr_int(src,(int * const *)res,(unsigned int)10 * sizeof(int *));
+  return;
+}
+
 /*@ requires aligned_end: len % 40 ≡ 0;
     requires
       valid_dest:
@@ -156,9 +320,13 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
   return __retres;
 }
 
-void nested(int (*dest)[10], int (*src)[10], size_t n)
+void nested(int (*src)[10], int (*dest)[10], int n)
 {
-  memcpy_arr10_int(dest,(int const (*)[10])src,n);
+  int (*res)[10] =
+    memcpy_arr10_int(dest,(int const (*)[10])src,
+                     (unsigned int)n * sizeof(int [10]));
+  memcpy_arr10_int(src,(int const (*)[10])res,
+                   (unsigned int)n * sizeof(int [10]));
   return;
 }
 
diff --git a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle b/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
index e6c64844a253de24791d81c903ecf9da780c3fa9..43e53fcefa4d1ae98f9c3c82d4cb6697452715e2 100644
--- a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
@@ -3,6 +3,11 @@
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+struct X {
+   int x ;
+   int y ;
+};
+typedef int named;
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -25,16 +30,78 @@ int *memmove_int(int *dest, int const *src, size_t len)
   return __retres;
 }
 
-int main(void)
+void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
 {
-  int __retres;
-  int dest[10];
-  int src[10] = {0};
-  int *p = memmove_int(dest,src,sizeof(src));
-  __retres = 0;
+  int *res = memmove_int(dest,src,(unsigned int)10 * sizeof(int));
+  memmove_int(src,res,(unsigned int)10 * sizeof(int));
+  return;
+}
+
+void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
+{
+  named *res = memmove_int(dest,src,(unsigned int)10 * sizeof(named));
+  memmove_int(src,res,(unsigned int)10 * sizeof(named));
+  return;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+    requires
+      valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
+    ensures
+      moved:
+        \let __fc_len = len / 8;
+        ∀ ℤ 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));
+    assigns \result \from dest;
+ */
+struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
+{
+  struct X *__retres;
+  __retres = (struct X *)memmove((void *)dest,(void const *)src,len);
   return __retres;
 }
 
+void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
+{
+  struct X *res = memmove_X(dest,src,(unsigned int)10 * sizeof(struct X));
+  memmove_X(src,res,(unsigned int)10 * sizeof(struct X));
+  return;
+}
+
+/*@ requires aligned_end: len % 4 ≡ 0;
+    requires
+      valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+    ensures
+      moved:
+        \let __fc_len = len / 4;
+        ∀ ℤ 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));
+    assigns \result \from dest;
+ */
+int **memmove_ptr_int(int **dest, int * const *src, size_t len)
+{
+  int **__retres;
+  __retres = (int **)memmove((void *)dest,(void const *)src,len);
+  return __retres;
+}
+
+void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
+{
+  int **res = memmove_ptr_int(dest,src,(unsigned int)10 * sizeof(int *));
+  memmove_ptr_int(src,res,(unsigned int)10 * sizeof(int *));
+  return;
+}
+
 /*@ requires aligned_end: len % 40 ≡ 0;
     requires
       valid_dest:
@@ -62,23 +129,36 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
   return __retres;
 }
 
-void nested(int (*dest)[10], int (*src)[10], size_t n)
+void nested(int (*src)[10], int (*dest)[10], int n)
 {
-  memmove_arr10_int(dest,src,n);
+  int (*res)[10] =
+    memmove_arr10_int(dest,src,(unsigned int)n * sizeof(int [10]));
+  memmove_arr10_int(src,res,(unsigned int)n * sizeof(int [10]));
   return;
 }
 
 
 [kernel] Parsing tests/functions/result/memmove.c (with preprocessing)
 [kernel] Parsing tests/functions/memmove.c (with preprocessing)
-[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:27 (sum 3742); keeping the one at tests/functions/result/memmove.c:27.
 [kernel] tests/functions/memmove.c:10: Warning: 
-  dropping duplicate def'n of func nested at tests/functions/memmove.c:10 in favor of that at tests/functions/result/memmove.c:64
+  dropping duplicate def'n of func integer at tests/functions/memmove.c:10 in favor of that at tests/functions/result/memmove.c:32
+[kernel] tests/functions/memmove.c:15: Warning: 
+  dropping duplicate def'n of func with_named at tests/functions/memmove.c:15 in favor of that at tests/functions/result/memmove.c:39
+[kernel] tests/functions/memmove.c:20: Warning: 
+  dropping duplicate def'n of func structure at tests/functions/memmove.c:20 in favor of that at tests/functions/result/memmove.c:68
+[kernel] tests/functions/memmove.c:25: Warning: 
+  dropping duplicate def'n of func pointers at tests/functions/memmove.c:25 in favor of that at tests/functions/result/memmove.c:97
+[kernel] tests/functions/memmove.c:30: Warning: 
+  dropping duplicate def'n of func nested at tests/functions/memmove.c:30 in favor of that at tests/functions/result/memmove.c:131
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
 #include "strings.h"
+struct X {
+   int x ;
+   int y ;
+};
+typedef int named;
 /*@ requires aligned_end: len % 4 ≡ 0;
     requires
       valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -102,16 +182,84 @@ int *memmove_int(int *dest, int const *src, size_t len)
   return __retres;
 }
 
-int main(void)
+void integer(int *src, int *dest)
+{
+  int *res =
+    memmove_int(dest,(int const *)src,(unsigned int)10 * sizeof(int));
+  memmove_int(src,(int const *)res,(unsigned int)10 * sizeof(int));
+  return;
+}
+
+void with_named(named *src, named *dest)
+{
+  named *res =
+    memmove_int(dest,(int const *)src,(unsigned int)10 * sizeof(named));
+  memmove_int(src,(int const *)res,(unsigned int)10 * sizeof(named));
+  return;
+}
+
+/*@ requires aligned_end: len % 8 ≡ 0;
+    requires
+      valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
+    ensures
+      moved:
+        \let __fc_len = \old(len) / 8;
+        ∀ ℤ 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));
+    assigns \result \from dest;
+ */
+struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
+{
+  struct X *__retres;
+  __retres = (struct X *)memmove((void *)dest,(void const *)src,len);
+  return __retres;
+}
+
+void structure(struct X *src, struct X *dest)
 {
-  int __retres;
-  int dest[10];
-  int src[10] = {0};
-  int *p = memmove_int(dest,(int const *)(src),sizeof(src));
-  __retres = 0;
+  struct X *res =
+    memmove_X(dest,(struct X const *)src,(unsigned int)10 * sizeof(struct X));
+  memmove_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+  return;
+}
+
+/*@ requires aligned_end: len % 4 ≡ 0;
+    requires
+      valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+    requires
+      valid_read_src:
+        \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+    ensures
+      moved:
+        \let __fc_len = \old(len) / 4;
+        ∀ ℤ 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));
+    assigns \result \from dest;
+ */
+int **memmove_ptr_int(int **dest, int * const *src, size_t len)
+{
+  int **__retres;
+  __retres = (int **)memmove((void *)dest,(void const *)src,len);
   return __retres;
 }
 
+void pointers(int **src, int **dest)
+{
+  int **res =
+    memmove_ptr_int(dest,(int * const *)src,(unsigned int)10 * sizeof(int *));
+  memmove_ptr_int(src,(int * const *)res,(unsigned int)10 * sizeof(int *));
+  return;
+}
+
 /*@ requires aligned_end: len % 40 ≡ 0;
     requires
       valid_dest:
@@ -140,9 +288,13 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
   return __retres;
 }
 
-void nested(int (*dest)[10], int (*src)[10], size_t n)
+void nested(int (*src)[10], int (*dest)[10], int n)
 {
-  memmove_arr10_int(dest,(int const (*)[10])src,n);
+  int (*res)[10] =
+    memmove_arr10_int(dest,(int const (*)[10])src,
+                      (unsigned int)n * sizeof(int [10]));
+  memmove_arr10_int(src,(int const (*)[10])res,
+                    (unsigned int)n * sizeof(int [10]));
   return;
 }