From 11d48df2883deaa124dd36f7a8bc4b1fe38a228c Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 10 Dec 2020 11:11:19 +0100
Subject: [PATCH] [instantiate] Update tests for new default machdep

---
 .../instantiate/tests/stdlib/no_fc_stdlib.c   |   3 +
 .../tests/stdlib/oracle/calloc.res.oracle     |  40 ++--
 .../tests/stdlib/oracle/malloc.res.oracle     |  32 +--
 .../tests/string/oracle/memcmp.res.oracle     |  68 +++---
 .../tests/string/oracle/memcpy.res.oracle     | 100 ++++-----
 .../tests/string/oracle/memmove.res.oracle    | 103 ++++-----
 .../tests/string/oracle/memset_0.res.oracle   | 116 +++++-----
 .../tests/string/oracle/memset_FF.res.oracle  | 202 +++++++++---------
 .../string/oracle/memset_value.res.oracle     |  98 ++++-----
 9 files changed, 388 insertions(+), 374 deletions(-)

diff --git a/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c b/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
index 21498c2ef2b..e23e00fa02e 100644
--- a/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
+++ b/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
@@ -1,3 +1,6 @@
+/* run.config
+  STDOPT: #"-machdep x86_32"
+ */
 #include <stddef.h>
 
 void* malloc(size_t s);
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
index 16706418268..e2656fb9461 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -300,17 +300,17 @@ int *calloc_int(size_t num, size_t size)
 int main(void)
 {
   int __retres;
-  int *pi = calloc_int((unsigned int)10,sizeof(int));
-  enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E));
-  float *pf = calloc_float((unsigned int)10,sizeof(float));
-  struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
-  char *pc = calloc_char((unsigned int)10,sizeof(char));
-  int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
+  int *pi = calloc_int((unsigned long)10,sizeof(int));
+  enum E *pe = calloc_e_E((unsigned long)10,sizeof(enum E));
+  float *pf = calloc_float((unsigned long)10,sizeof(float));
+  struct X *px = calloc_st_X((unsigned long)10,sizeof(struct X));
+  char *pc = calloc_char((unsigned long)10,sizeof(char));
+  int (*pa)[10] = calloc_arr10_int((unsigned long)10,sizeof(int [10]));
   struct Flex *f =
-    calloc_st_Flex((unsigned int)1,
-                   sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
-  void *v = calloc((unsigned int)10,sizeof(char));
-  struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
+    calloc_st_Flex((unsigned long)1,
+                   sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
+  void *v = calloc((unsigned long)10,sizeof(char));
+  struct incomplete *inc = calloc((unsigned long)10,(unsigned long)10);
   __retres = 0;
   return __retres;
 }
@@ -619,17 +619,17 @@ int *calloc_int(size_t num, size_t size)
 int main(void)
 {
   int __retres;
-  int *pi = calloc_int((unsigned int)10,sizeof(int));
-  enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E));
-  float *pf = calloc_float((unsigned int)10,sizeof(float));
-  struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
-  char *pc = calloc_char((unsigned int)10,sizeof(char));
-  int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
+  int *pi = calloc_int((unsigned long)10,sizeof(int));
+  enum E *pe = calloc_e_E((unsigned long)10,sizeof(enum E));
+  float *pf = calloc_float((unsigned long)10,sizeof(float));
+  struct X *px = calloc_st_X((unsigned long)10,sizeof(struct X));
+  char *pc = calloc_char((unsigned long)10,sizeof(char));
+  int (*pa)[10] = calloc_arr10_int((unsigned long)10,sizeof(int [10]));
   struct Flex *f =
-    calloc_st_Flex((unsigned int)1,
-                   sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
-  void *v = calloc((unsigned int)10,sizeof(char));
-  struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
+    calloc_st_Flex((unsigned long)1,
+                   sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
+  void *v = calloc((unsigned long)10,sizeof(char));
+  struct incomplete *inc = calloc((unsigned long)10,(unsigned long)10);
   __retres = 0;
   return __retres;
 }
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
index 9aff502467c..5fc593cb30d 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
@@ -204,15 +204,15 @@ int *malloc_int(size_t size)
 int main(void)
 {
   int __retres;
-  int *pi = malloc_int(sizeof(int) * (unsigned int)10);
-  float *pf = malloc_float(sizeof(float) * (unsigned int)10);
-  struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
-  char *pc = malloc_char((unsigned int)10);
-  int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
+  int *pi = malloc_int(sizeof(int) * (unsigned long)10);
+  float *pf = malloc_float(sizeof(float) * (unsigned long)10);
+  struct X *px = malloc_st_X(sizeof(struct X) * (unsigned long)10);
+  char *pc = malloc_char((unsigned long)10);
+  int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned long)10);
   struct Flex *f =
-    malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
-  void *v = malloc(sizeof(char) * (unsigned int)10);
-  struct incomplete *inc = malloc((unsigned int)10);
+    malloc_st_Flex(sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
+  void *v = malloc(sizeof(char) * (unsigned long)10);
+  struct incomplete *inc = malloc((unsigned long)10);
   __retres = 0;
   return __retres;
 }
@@ -420,15 +420,15 @@ int *malloc_int(size_t size)
 int main(void)
 {
   int __retres;
-  int *pi = malloc_int(sizeof(int) * (unsigned int)10);
-  float *pf = malloc_float(sizeof(float) * (unsigned int)10);
-  struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
-  char *pc = malloc_char((unsigned int)10);
-  int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
+  int *pi = malloc_int(sizeof(int) * (unsigned long)10);
+  float *pf = malloc_float(sizeof(float) * (unsigned long)10);
+  struct X *px = malloc_st_X(sizeof(struct X) * (unsigned long)10);
+  char *pc = malloc_char((unsigned long)10);
+  int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned long)10);
   struct Flex *f =
-    malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
-  void *v = malloc(sizeof(char) * (unsigned int)10);
-  struct incomplete *inc = malloc((unsigned int)10);
+    malloc_st_Flex(sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
+  void *v = malloc(sizeof(char) * (unsigned long)10);
+  struct incomplete *inc = malloc((unsigned long)10);
   __retres = 0;
   return __retres;
 }
diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
index 1f82bcd57b0..dd2862c8e5f 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
@@ -48,14 +48,14 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
 int integer(int * /*[10]*/ s1, int * /*[10]*/ s2)
 {
   int tmp;
-  tmp = memcmp_int(s1,s2,(unsigned int)10 * sizeof(int));
+  tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(int));
   return tmp;
 }
 
 int with_named(named * /*[10]*/ s1, named * /*[10]*/ s2)
 {
   int tmp;
-  tmp = memcmp_int(s1,s2,(unsigned int)10 * sizeof(named));
+  tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(named));
   return tmp;
 }
 
@@ -86,26 +86,26 @@ int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
 int structure(struct X * /*[10]*/ s1, struct X * /*[10]*/ s2)
 {
   int tmp;
-  tmp = memcmp_st_X(s1,s2,(unsigned int)10 * sizeof(struct X));
+  tmp = memcmp_st_X(s1,s2,(unsigned long)10 * sizeof(struct X));
   return tmp;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
       valid_read_s1:
-        \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1));
+        \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
     requires
       valid_read_s2:
-        \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1));
+        \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
     ensures
       equals:
-        \let __fc_len = len / 4;
+        \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 / 4 - 1))),
-            (indirect: *(s2 + (0 .. len / 4 - 1)));
+      \from (indirect: *(s1 + (0 .. len / 8 - 1))),
+            (indirect: *(s2 + (0 .. len / 8 - 1)));
  */
 int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
 {
@@ -117,7 +117,7 @@ int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
 int pointers(int ** /*[10]*/ s1, int ** /*[10]*/ s2)
 {
   int tmp;
-  tmp = memcmp_ptr_int(s1,s2,(unsigned int)10 * sizeof(int *));
+  tmp = memcmp_ptr_int(s1,s2,(unsigned long)10 * sizeof(int *));
   return tmp;
 }
 
@@ -151,32 +151,32 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
 int nested(int (*s1)[10], int (*s2)[10], int n)
 {
   int tmp;
-  tmp = memcmp_arr10_int(s1,s2,(unsigned int)n * sizeof(int [10]));
+  tmp = memcmp_arr10_int(s1,s2,(unsigned long)n * sizeof(int [10]));
   return tmp;
 }
 
 int with_void(void *s1, void *s2, int n)
 {
   int tmp;
-  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)10);
+  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)10);
   return tmp;
 }
 
 int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
 {
   int tmp;
-  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
+  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)n);
   return tmp;
 }
 
 void with_null_or_int(int * /*[10]*/ p)
 {
-  memcmp((void const *)0,(void const *)p,(unsigned int)10 * sizeof(int));
-  memcmp((void const *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+  memcmp((void const *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+  memcmp((void const *)p,(void const *)0,(unsigned long)10 * sizeof(int));
   memcmp((void const *)((int const *)42),(void const *)p,
-         (unsigned int)10 * sizeof(int));
+         (unsigned long)10 * sizeof(int));
   memcmp((void const *)p,(void const *)((int const *)42),
-         (unsigned int)10 * sizeof(int));
+         (unsigned long)10 * sizeof(int));
   return;
 }
 
@@ -221,7 +221,7 @@ int integer(int *s1, int *s2)
 {
   int tmp;
   tmp = memcmp_int((int const *)s1,(int const *)s2,
-                   (unsigned int)10 * sizeof(int));
+                   (unsigned long)10 * sizeof(int));
   return tmp;
 }
 
@@ -229,7 +229,7 @@ int with_named(named *s1, named *s2)
 {
   int tmp;
   tmp = memcmp_int((int const *)s1,(int const *)s2,
-                   (unsigned int)10 * sizeof(named));
+                   (unsigned long)10 * sizeof(named));
   return tmp;
 }
 
@@ -262,27 +262,27 @@ int structure(struct X *s1, struct X *s2)
 {
   int tmp;
   tmp = memcmp_st_X((struct X const *)s1,(struct X const *)s2,
-                    (unsigned int)10 * sizeof(struct X));
+                    (unsigned long)10 * sizeof(struct X));
   return tmp;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
       valid_read_s1:
-        \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1));
+        \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
     requires
       valid_read_s2:
-        \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1));
+        \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
     ensures
       equals:
-        \let __fc_len = \old(len) / 4;
+        \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 / 4 - 1))),
-            (indirect: *(s2 + (0 .. len / 4 - 1)));
+      \from (indirect: *(s1 + (0 .. len / 8 - 1))),
+            (indirect: *(s2 + (0 .. len / 8 - 1)));
  */
 int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
 {
@@ -295,7 +295,7 @@ int pointers(int **s1, int **s2)
 {
   int tmp;
   tmp = memcmp_ptr_int((int * const *)s1,(int * const *)s2,
-                       (unsigned int)10 * sizeof(int *));
+                       (unsigned long)10 * sizeof(int *));
   return tmp;
 }
 
@@ -331,32 +331,32 @@ int nested(int (*s1)[10], int (*s2)[10], int n)
 {
   int tmp;
   tmp = memcmp_arr10_int((int const (*)[10])s1,(int const (*)[10])s2,
-                         (unsigned int)n * sizeof(int [10]));
+                         (unsigned long)n * sizeof(int [10]));
   return tmp;
 }
 
 int with_void(void *s1, void *s2, int n)
 {
   int tmp;
-  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)10);
+  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)10);
   return tmp;
 }
 
 int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
 {
   int tmp;
-  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
+  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)n);
   return tmp;
 }
 
 void with_null_or_int(int *p)
 {
-  memcmp((void const *)0,(void const *)p,(unsigned int)10 * sizeof(int));
-  memcmp((void const *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+  memcmp((void const *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+  memcmp((void const *)p,(void const *)0,(unsigned long)10 * sizeof(int));
   memcmp((void const *)((int const *)42),(void const *)p,
-         (unsigned int)10 * sizeof(int));
+         (unsigned long)10 * sizeof(int));
   memcmp((void const *)p,(void const *)((int const *)42),
-         (unsigned int)10 * sizeof(int));
+         (unsigned long)10 * sizeof(int));
   return;
 }
 
diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 899dd8afefc..259a1cacb16 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
@@ -53,15 +53,15 @@ int *memcpy_int(int *dest, int const *src, size_t len)
 
 void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
 {
-  int *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(int));
-  memcpy_int(src,res,(unsigned int)10 * sizeof(int));
+  int *res = memcpy_int(dest,src,(unsigned long)10 * sizeof(int));
+  memcpy_int(src,res,(unsigned long)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));
+  named *res = memcpy_int(dest,src,(unsigned long)10 * sizeof(named));
+  memcpy_int(src,res,(unsigned long)10 * sizeof(named));
   return;
 }
 
@@ -93,28 +93,28 @@ struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
 
 void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
 {
-  struct X *res = memcpy_st_X(dest,src,(unsigned int)10 * sizeof(struct X));
-  memcpy_st_X(src,res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memcpy_st_X(dest,src,(unsigned long)10 * sizeof(struct X));
+  memcpy_st_X(src,res,(unsigned long)10 * sizeof(struct X));
   return;
 }
 
 /*@ requires
       separation:
-        \let __fc_len = len / 4;
+        \let __fc_len = len / 8;
           \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
-    requires aligned_end: len % 4 ≡ 0;
+    requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
     requires
       valid_read_src:
-        \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+        \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
     ensures
       copied:
-        \let __fc_len = len / 4;
+        \let __fc_len = len / 8;
         ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
     ensures result: \result ≡ dest;
-    assigns *(dest + (0 .. len / 4 - 1)), \result;
-    assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
+    assigns *(dest + (0 .. len / 8 - 1)), \result;
+    assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
     assigns \result \from dest;
  */
 int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
@@ -126,8 +126,8 @@ int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
 
 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 *));
+  int **res = memcpy_ptr_int(dest,src,(unsigned long)10 * sizeof(int *));
+  memcpy_ptr_int(src,res,(unsigned long)10 * sizeof(int *));
   return;
 }
 
@@ -165,32 +165,32 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
 void nested(int (*src)[10], int (*dest)[10], int 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]));
+    memcpy_arr10_int(dest,src,(unsigned long)n * sizeof(int [10]));
+  memcpy_arr10_int(src,res,(unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *src, void *dest, int n)
 {
-  void *res = memcpy(dest,(void const *)src,(unsigned int)n);
-  memcpy(src,(void const *)res,(unsigned int)n);
+  void *res = memcpy(dest,(void const *)src,(unsigned long)n);
+  memcpy(src,(void const *)res,(unsigned long)n);
   return;
 }
 
 void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
 {
   struct incomplete *res =
-    memcpy((void *)dest,(void const *)src,(unsigned int)n);
-  memcpy((void *)src,(void const *)res,(unsigned int)n);
+    memcpy((void *)dest,(void const *)src,(unsigned long)n);
+  memcpy((void *)src,(void const *)res,(unsigned long)n);
   return;
 }
 
 void with_null_or_int(int * /*[10]*/ p)
 {
-  memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
-  memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
-  memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
-  memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+  memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+  memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
+  memcpy((void *)((int *)42),(void const *)p,(unsigned long)10 * sizeof(int));
+  memcpy((void *)p,(void const *)((int *)42),(unsigned long)10 * sizeof(int));
   return;
 }
 
@@ -236,16 +236,16 @@ int *memcpy_int(int *dest, int const *src, size_t len)
 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));
+    memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(int));
+  memcpy_int(src,(int const *)res,(unsigned long)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));
+    memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(named));
+  memcpy_int(src,(int const *)res,(unsigned long)10 * sizeof(named));
   return;
 }
 
@@ -280,29 +280,29 @@ void structure(struct X *src, struct X *dest)
 {
   struct X *res =
     memcpy_st_X(dest,(struct X const *)src,
-                (unsigned int)10 * sizeof(struct X));
-  memcpy_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+                (unsigned long)10 * sizeof(struct X));
+  memcpy_st_X(src,(struct X const *)res,(unsigned long)10 * sizeof(struct X));
   return;
 }
 
 /*@ requires
       separation:
-        \let __fc_len = len / 4;
+        \let __fc_len = len / 8;
           \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
-    requires aligned_end: len % 4 ≡ 0;
+    requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
     requires
       valid_read_src:
-        \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+        \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
     ensures
       copied:
-        \let __fc_len = \old(len) / 4;
+        \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 / 4 - 1)), \result;
-    assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
+    assigns *(dest + (0 .. len / 8 - 1)), \result;
+    assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
     assigns \result \from dest;
  */
 int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
@@ -315,8 +315,8 @@ int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
 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 *));
+    memcpy_ptr_int(dest,(int * const *)src,(unsigned long)10 * sizeof(int *));
+  memcpy_ptr_int(src,(int * const *)res,(unsigned long)10 * sizeof(int *));
   return;
 }
 
@@ -356,33 +356,33 @@ void nested(int (*src)[10], int (*dest)[10], int n)
 {
   int (*res)[10] =
     memcpy_arr10_int(dest,(int const (*)[10])src,
-                     (unsigned int)n * sizeof(int [10]));
+                     (unsigned long)n * sizeof(int [10]));
   memcpy_arr10_int(src,(int const (*)[10])res,
-                   (unsigned int)n * sizeof(int [10]));
+                   (unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *src, void *dest, int n)
 {
-  void *res = memcpy(dest,(void const *)src,(unsigned int)n);
-  memcpy(src,(void const *)res,(unsigned int)n);
+  void *res = memcpy(dest,(void const *)src,(unsigned long)n);
+  memcpy(src,(void const *)res,(unsigned long)n);
   return;
 }
 
 void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
 {
   struct incomplete *res =
-    memcpy((void *)dest,(void const *)src,(unsigned int)n);
-  memcpy((void *)src,(void const *)res,(unsigned int)n);
+    memcpy((void *)dest,(void const *)src,(unsigned long)n);
+  memcpy((void *)src,(void const *)res,(unsigned long)n);
   return;
 }
 
 void with_null_or_int(int *p)
 {
-  memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
-  memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
-  memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
-  memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+  memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+  memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
+  memcpy((void *)((int *)42),(void const *)p,(unsigned long)10 * sizeof(int));
+  memcpy((void *)p,(void const *)((int *)42),(unsigned long)10 * sizeof(int));
   return;
 }
 
diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
index f327581499b..fc4bf692213 100644
--- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
@@ -49,15 +49,15 @@ int *memmove_int(int *dest, int const *src, size_t len)
 
 void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
 {
-  int *res = memmove_int(dest,src,(unsigned int)10 * sizeof(int));
-  memmove_int(src,res,(unsigned int)10 * sizeof(int));
+  int *res = memmove_int(dest,src,(unsigned long)10 * sizeof(int));
+  memmove_int(src,res,(unsigned long)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));
+  named *res = memmove_int(dest,src,(unsigned long)10 * sizeof(named));
+  memmove_int(src,res,(unsigned long)10 * sizeof(named));
   return;
 }
 
@@ -85,24 +85,25 @@ struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
 
 void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
 {
-  struct X *res = memmove_st_X(dest,src,(unsigned int)10 * sizeof(struct X));
-  memmove_st_X(src,res,(unsigned int)10 * sizeof(struct X));
+  struct X *res =
+    memmove_st_X(dest,src,(unsigned long)10 * sizeof(struct X));
+  memmove_st_X(src,res,(unsigned long)10 * sizeof(struct X));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
     requires
       valid_read_src:
-        \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+        \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
     ensures
       moved:
-        \let __fc_len = len / 4;
+        \let __fc_len = len / 8;
         ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
     ensures result: \result ≡ dest;
-    assigns *(dest + (0 .. len / 4 - 1)), \result;
-    assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
+    assigns *(dest + (0 .. len / 8 - 1)), \result;
+    assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
     assigns \result \from dest;
  */
 int **memmove_ptr_int(int **dest, int * const *src, size_t len)
@@ -114,8 +115,8 @@ int **memmove_ptr_int(int **dest, int * const *src, size_t len)
 
 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 *));
+  int **res = memmove_ptr_int(dest,src,(unsigned long)10 * sizeof(int *));
+  memmove_ptr_int(src,res,(unsigned long)10 * sizeof(int *));
   return;
 }
 
@@ -149,32 +150,34 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
 void nested(int (*src)[10], int (*dest)[10], int 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]));
+    memmove_arr10_int(dest,src,(unsigned long)n * sizeof(int [10]));
+  memmove_arr10_int(src,res,(unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *src, void *dest, int n)
 {
-  void *res = memmove(dest,(void const *)src,(unsigned int)n);
-  memmove(src,(void const *)res,(unsigned int)n);
+  void *res = memmove(dest,(void const *)src,(unsigned long)n);
+  memmove(src,(void const *)res,(unsigned long)n);
   return;
 }
 
 void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
 {
   struct incomplete *res =
-    memmove((void *)dest,(void const *)src,(unsigned int)n);
-  memmove((void *)src,(void const *)res,(unsigned int)n);
+    memmove((void *)dest,(void const *)src,(unsigned long)n);
+  memmove((void *)src,(void const *)res,(unsigned long)n);
   return;
 }
 
 void with_null_or_int(int * /*[10]*/ p)
 {
-  memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
-  memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
-  memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
-  memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+  memmove((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+  memmove((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
+  memmove((void *)((int *)42),(void const *)p,
+          (unsigned long)10 * sizeof(int));
+  memmove((void *)p,(void const *)((int *)42),
+          (unsigned long)10 * sizeof(int));
   return;
 }
 
@@ -216,16 +219,16 @@ int *memmove_int(int *dest, int const *src, size_t len)
 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));
+    memmove_int(dest,(int const *)src,(unsigned long)10 * sizeof(int));
+  memmove_int(src,(int const *)res,(unsigned long)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));
+    memmove_int(dest,(int const *)src,(unsigned long)10 * sizeof(named));
+  memmove_int(src,(int const *)res,(unsigned long)10 * sizeof(named));
   return;
 }
 
@@ -256,25 +259,26 @@ void structure(struct X *src, struct X *dest)
 {
   struct X *res =
     memmove_st_X(dest,(struct X const *)src,
-                 (unsigned int)10 * sizeof(struct X));
-  memmove_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+                 (unsigned long)10 * sizeof(struct X));
+  memmove_st_X(src,(struct X const *)res,
+               (unsigned long)10 * sizeof(struct X));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
     requires
       valid_read_src:
-        \let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
+        \let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
     ensures
       moved:
-        \let __fc_len = \old(len) / 4;
+        \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 / 4 - 1)), \result;
-    assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
+    assigns *(dest + (0 .. len / 8 - 1)), \result;
+    assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
     assigns \result \from dest;
  */
 int **memmove_ptr_int(int **dest, int * const *src, size_t len)
@@ -287,8 +291,9 @@ int **memmove_ptr_int(int **dest, int * const *src, size_t len)
 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 *));
+    memmove_ptr_int(dest,(int * const *)src,
+                    (unsigned long)10 * sizeof(int *));
+  memmove_ptr_int(src,(int * const *)res,(unsigned long)10 * sizeof(int *));
   return;
 }
 
@@ -324,33 +329,35 @@ void nested(int (*src)[10], int (*dest)[10], int n)
 {
   int (*res)[10] =
     memmove_arr10_int(dest,(int const (*)[10])src,
-                      (unsigned int)n * sizeof(int [10]));
+                      (unsigned long)n * sizeof(int [10]));
   memmove_arr10_int(src,(int const (*)[10])res,
-                    (unsigned int)n * sizeof(int [10]));
+                    (unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *src, void *dest, int n)
 {
-  void *res = memmove(dest,(void const *)src,(unsigned int)n);
-  memmove(src,(void const *)res,(unsigned int)n);
+  void *res = memmove(dest,(void const *)src,(unsigned long)n);
+  memmove(src,(void const *)res,(unsigned long)n);
   return;
 }
 
 void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
 {
   struct incomplete *res =
-    memmove((void *)dest,(void const *)src,(unsigned int)n);
-  memmove((void *)src,(void const *)res,(unsigned int)n);
+    memmove((void *)dest,(void const *)src,(unsigned long)n);
+  memmove((void *)src,(void const *)res,(unsigned long)n);
   return;
 }
 
 void with_null_or_int(int *p)
 {
-  memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
-  memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
-  memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
-  memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+  memmove((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
+  memmove((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
+  memmove((void *)((int *)42),(void const *)p,
+          (unsigned long)10 * sizeof(int));
+  memmove((void *)p,(void const *)((int *)42),
+          (unsigned long)10 * sizeof(int));
   return;
 }
 
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
index dae2db7eba3..f0925319e77 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
@@ -39,8 +39,8 @@ char *memset_char(char *ptr, char value, size_t len)
 
 void chars(char * /*[10]*/ dest)
 {
-  char *res = memset_char(dest,(char)0,(unsigned int)10);
-  memset_char(res,(char)0,(unsigned int)10);
+  char *res = memset_char(dest,(char)0,(unsigned long)10);
+  memset_char(res,(char)0,(unsigned long)10);
   return;
 }
 
@@ -63,8 +63,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
 
 void uchars(unsigned char * /*[10]*/ dest)
 {
-  unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned int)10);
-  memset_uchar(res,(unsigned char)0,(unsigned int)10);
+  unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned long)10);
+  memset_uchar(res,(unsigned char)0,(unsigned long)10);
   return;
 }
 
@@ -91,8 +91,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
 
 void nested_chars(char (* /*[10]*/ dest)[10])
 {
-  char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned int)100);
-  memset_arr10_char(res,(char)0,(unsigned int)100);
+  char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned long)100);
+  memset_arr10_char(res,(char)0,(unsigned long)100);
   return;
 }
 
@@ -117,8 +117,8 @@ int *memset_int_0(int *ptr, size_t len)
 
 void integer(int * /*[10]*/ dest)
 {
-  int *res = memset_int_0(dest,(unsigned int)10 * sizeof(int));
-  memset_int_0(res,(unsigned int)10 * sizeof(int));
+  int *res = memset_int_0(dest,(unsigned long)10 * sizeof(int));
+  memset_int_0(res,(unsigned long)10 * sizeof(int));
   return;
 }
 
@@ -143,8 +143,8 @@ enum E *memset_e_E_0(enum E *ptr, size_t len)
 
 void with_enum(enum E * /*[10]*/ dest)
 {
-  enum E *res = memset_e_E_0(dest,(unsigned int)10 * sizeof(enum E));
-  memset_e_E_0(res,(unsigned int)10 * sizeof(enum E));
+  enum E *res = memset_e_E_0(dest,(unsigned long)10 * sizeof(enum E));
+  memset_e_E_0(res,(unsigned long)10 * sizeof(enum E));
   return;
 }
 
@@ -169,15 +169,15 @@ float *memset_float_0(float *ptr, size_t len)
 
 void floats(float * /*[10]*/ dest)
 {
-  float *res = memset_float_0(dest,(unsigned int)10 * sizeof(float));
-  memset_float_0(res,(unsigned int)10 * sizeof(float));
+  float *res = memset_float_0(dest,(unsigned long)10 * sizeof(float));
+  memset_float_0(res,(unsigned long)10 * sizeof(float));
   return;
 }
 
 void with_named(named * /*[10]*/ dest)
 {
-  named *res = memset_int_0(dest,(unsigned int)10 * sizeof(named));
-  memset_int_0(res,(unsigned int)10 * sizeof(named));
+  named *res = memset_int_0(dest,(unsigned long)10 * sizeof(named));
+  memset_int_0(res,(unsigned long)10 * sizeof(named));
   return;
 }
 
@@ -203,21 +203,21 @@ struct X *memset_st_X_0(struct X *ptr, size_t len)
 
 void structure(struct X * /*[10]*/ dest)
 {
-  struct X *res = memset_st_X_0(dest,(unsigned int)10 * sizeof(struct X));
-  memset_st_X_0(res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memset_st_X_0(dest,(unsigned long)10 * sizeof(struct X));
+  memset_st_X_0(res,(unsigned long)10 * sizeof(struct X));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
     ensures
       set_content:
-        \let __fc_len = len / 4;
+        \let __fc_len = len / 8;
         ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ \null;
     ensures result: \result ≡ ptr;
-    assigns *(ptr + (0 .. len / 4 - 1)), \result;
-    assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+    assigns *(ptr + (0 .. len / 8 - 1)), \result;
+    assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
     assigns \result \from ptr;
  */
 int **memset_ptr_int_0(int **ptr, size_t len)
@@ -229,8 +229,8 @@ int **memset_ptr_int_0(int **ptr, size_t len)
 
 void pointers(int ** /*[10]*/ dest)
 {
-  int **res = memset_ptr_int_0(dest,(unsigned int)10 * sizeof(int *));
-  memset_ptr_int_0(res,(unsigned int)10 * sizeof(int *));
+  int **res = memset_ptr_int_0(dest,(unsigned long)10 * sizeof(int *));
+  memset_ptr_int_0(res,(unsigned long)10 * sizeof(int *));
   return;
 }
 
@@ -258,22 +258,22 @@ int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10]
 void nested(int (*dest)[10], int n)
 {
   int (*res)[10] =
-    memset_arr10_int_0(dest,(unsigned int)n * sizeof(int [10]));
-  memset_arr10_int_0(res,(unsigned int)n * sizeof(int [10]));
+    memset_arr10_int_0(dest,(unsigned long)n * sizeof(int [10]));
+  memset_arr10_int_0(res,(unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *dest)
 {
-  void *res = memset(dest,0,(unsigned int)10);
-  memset(res,0,(unsigned int)10);
+  void *res = memset(dest,0,(unsigned long)10);
+  memset(res,0,(unsigned long)10);
   return;
 }
 
 void with_null_or_int(void)
 {
-  memset((void *)0,0,(unsigned int)10);
-  memset((void *)((int *)42),0,(unsigned int)10);
+  memset((void *)0,0,(unsigned long)10);
+  memset((void *)((int *)42),0,(unsigned long)10);
   return;
 }
 
@@ -313,8 +313,8 @@ char *memset_char(char *ptr, char value, size_t len)
 
 void chars(char *dest)
 {
-  char *res = memset_char(dest,(char)0,(unsigned int)10);
-  memset_char(res,(char)0,(unsigned int)10);
+  char *res = memset_char(dest,(char)0,(unsigned long)10);
+  memset_char(res,(char)0,(unsigned long)10);
   return;
 }
 
@@ -339,8 +339,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
 
 void uchars(unsigned char *dest)
 {
-  unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned int)10);
-  memset_uchar(res,(unsigned char)0,(unsigned int)10);
+  unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned long)10);
+  memset_uchar(res,(unsigned char)0,(unsigned long)10);
   return;
 }
 
@@ -368,8 +368,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
 
 void nested_chars(char (*dest)[10])
 {
-  char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned int)100);
-  memset_arr10_char(res,(char)0,(unsigned int)100);
+  char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned long)100);
+  memset_arr10_char(res,(char)0,(unsigned long)100);
   return;
 }
 
@@ -394,8 +394,8 @@ int *memset_int_0(int *ptr, size_t len)
 
 void integer(int *dest)
 {
-  int *res = memset_int_0(dest,(unsigned int)10 * sizeof(int));
-  memset_int_0(res,(unsigned int)10 * sizeof(int));
+  int *res = memset_int_0(dest,(unsigned long)10 * sizeof(int));
+  memset_int_0(res,(unsigned long)10 * sizeof(int));
   return;
 }
 
@@ -420,8 +420,8 @@ enum E *memset_e_E_0(enum E *ptr, size_t len)
 
 void with_enum(enum E *dest)
 {
-  enum E *res = memset_e_E_0(dest,(unsigned int)10 * sizeof(enum E));
-  memset_e_E_0(res,(unsigned int)10 * sizeof(enum E));
+  enum E *res = memset_e_E_0(dest,(unsigned long)10 * sizeof(enum E));
+  memset_e_E_0(res,(unsigned long)10 * sizeof(enum E));
   return;
 }
 
@@ -446,15 +446,15 @@ float *memset_float_0(float *ptr, size_t len)
 
 void floats(float *dest)
 {
-  float *res = memset_float_0(dest,(unsigned int)10 * sizeof(float));
-  memset_float_0(res,(unsigned int)10 * sizeof(float));
+  float *res = memset_float_0(dest,(unsigned long)10 * sizeof(float));
+  memset_float_0(res,(unsigned long)10 * sizeof(float));
   return;
 }
 
 void with_named(named *dest)
 {
-  named *res = memset_int_0(dest,(unsigned int)10 * sizeof(named));
-  memset_int_0(res,(unsigned int)10 * sizeof(named));
+  named *res = memset_int_0(dest,(unsigned long)10 * sizeof(named));
+  memset_int_0(res,(unsigned long)10 * sizeof(named));
   return;
 }
 
@@ -481,21 +481,21 @@ struct X *memset_st_X_0(struct X *ptr, size_t len)
 
 void structure(struct X *dest)
 {
-  struct X *res = memset_st_X_0(dest,(unsigned int)10 * sizeof(struct X));
-  memset_st_X_0(res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memset_st_X_0(dest,(unsigned long)10 * sizeof(struct X));
+  memset_st_X_0(res,(unsigned long)10 * sizeof(struct X));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
     ensures
       set_content:
-        \let __fc_len = \old(len) / 4;
+        \let __fc_len = \old(len) / 8;
         ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ \null;
     ensures result: \result ≡ \old(ptr);
-    assigns *(ptr + (0 .. len / 4 - 1)), \result;
-    assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+    assigns *(ptr + (0 .. len / 8 - 1)), \result;
+    assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
     assigns \result \from ptr;
  */
 int **memset_ptr_int_0(int **ptr, size_t len)
@@ -507,8 +507,8 @@ int **memset_ptr_int_0(int **ptr, size_t len)
 
 void pointers(int **dest)
 {
-  int **res = memset_ptr_int_0(dest,(unsigned int)10 * sizeof(int *));
-  memset_ptr_int_0(res,(unsigned int)10 * sizeof(int *));
+  int **res = memset_ptr_int_0(dest,(unsigned long)10 * sizeof(int *));
+  memset_ptr_int_0(res,(unsigned long)10 * sizeof(int *));
   return;
 }
 
@@ -536,22 +536,22 @@ int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10]
 void nested(int (*dest)[10], int n)
 {
   int (*res)[10] =
-    memset_arr10_int_0(dest,(unsigned int)n * sizeof(int [10]));
-  memset_arr10_int_0(res,(unsigned int)n * sizeof(int [10]));
+    memset_arr10_int_0(dest,(unsigned long)n * sizeof(int [10]));
+  memset_arr10_int_0(res,(unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *dest)
 {
-  void *res = memset(dest,0,(unsigned int)10);
-  memset(res,0,(unsigned int)10);
+  void *res = memset(dest,0,(unsigned long)10);
+  memset(res,0,(unsigned long)10);
   return;
 }
 
 void with_null_or_int(void)
 {
-  memset((void *)0,0,(unsigned int)10);
-  memset((void *)((int *)42),0,(unsigned int)10);
+  memset((void *)0,0,(unsigned long)10);
+  memset((void *)((int *)42),0,(unsigned long)10);
   return;
 }
 
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
index 137dd1c21a0..798296c18a9 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -39,8 +39,8 @@ char *memset_char(char *ptr, char value, size_t len)
 
 void chars(char * /*[10]*/ dest)
 {
-  char *res = memset_char(dest,(char)0xFF,(unsigned int)10);
-  memset_char(res,(char)0xFF,(unsigned int)10);
+  char *res = memset_char(dest,(char)0xFF,(unsigned long)10);
+  memset_char(res,(char)0xFF,(unsigned long)10);
   return;
 }
 
@@ -64,8 +64,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
 void uchars(unsigned char * /*[10]*/ dest)
 {
   unsigned char *res =
-    memset_uchar(dest,(unsigned char)0xFF,(unsigned int)10);
-  memset_uchar(res,(unsigned char)0xFF,(unsigned int)10);
+    memset_uchar(dest,(unsigned char)0xFF,(unsigned long)10);
+  memset_uchar(res,(unsigned char)0xFF,(unsigned long)10);
   return;
 }
 
@@ -92,8 +92,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
 
 void nested_chars(char (* /*[10]*/ dest)[10])
 {
-  char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned int)100);
-  memset_arr10_char(res,(char)0xFF,(unsigned int)100);
+  char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned long)100);
+  memset_arr10_char(res,(char)0xFF,(unsigned long)100);
   return;
 }
 
@@ -118,8 +118,8 @@ int *memset_int_FF(int *ptr, size_t len)
 
 void integer(int * /*[10]*/ dest)
 {
-  int *res = memset_int_FF(dest,(unsigned int)10 * sizeof(int));
-  memset_int_FF(res,(unsigned int)10 * sizeof(int));
+  int *res = memset_int_FF(dest,(unsigned long)10 * sizeof(int));
+  memset_int_FF(res,(unsigned long)10 * sizeof(int));
   return;
 }
 
@@ -144,8 +144,8 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len)
 
 void with_enum(enum E * /*[10]*/ dest)
 {
-  enum E *res = memset_e_E_FF(dest,(unsigned int)10 * sizeof(enum E));
-  memset_e_E_FF(res,(unsigned int)10 * sizeof(enum E));
+  enum E *res = memset_e_E_FF(dest,(unsigned long)10 * sizeof(enum E));
+  memset_e_E_FF(res,(unsigned long)10 * sizeof(enum E));
   return;
 }
 
@@ -171,21 +171,21 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
 void unsigned_integer(unsigned int * /*[10]*/ dest)
 {
   unsigned int *res =
-    memset_uint_FF(dest,(unsigned int)10 * sizeof(unsigned int));
-  memset_uint_FF(res,(unsigned int)10 * sizeof(unsigned int));
+    memset_uint_FF(dest,(unsigned long)10 * sizeof(unsigned int));
+  memset_uint_FF(res,(unsigned long)10 * sizeof(unsigned int));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
     ensures
       set_content:
-        \let __fc_len = len / 4;
+        \let __fc_len = len / 8;
         ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((long)0);
     ensures result: \result ≡ ptr;
-    assigns *(ptr + (0 .. len / 4 - 1)), \result;
-    assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+    assigns *(ptr + (0 .. len / 8 - 1)), \result;
+    assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
     assigns \result \from ptr;
  */
 long *memset_long_FF(long *ptr, size_t len)
@@ -197,21 +197,22 @@ long *memset_long_FF(long *ptr, size_t len)
 
 void long_integer(long * /*[10]*/ dest)
 {
-  long *res = memset_long_FF(dest,(unsigned int)10 * sizeof(long));
-  memset_long_FF(res,(unsigned int)10 * sizeof(long));
+  long *res = memset_long_FF(dest,(unsigned long)10 * sizeof(long));
+  memset_long_FF(res,(unsigned long)10 * sizeof(long));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
     ensures
       set_content:
-        \let __fc_len = len / 4;
-        ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 4294967295;
+        \let __fc_len = len / 8;
+        ∀ ℤ j0;
+          0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 18446744073709551615;
     ensures result: \result ≡ ptr;
-    assigns *(ptr + (0 .. len / 4 - 1)), \result;
-    assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+    assigns *(ptr + (0 .. len / 8 - 1)), \result;
+    assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
     assigns \result \from ptr;
  */
 unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
@@ -224,8 +225,8 @@ unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
 void unsigned_long_integer(unsigned long * /*[10]*/ dest)
 {
   unsigned long *res =
-    memset_ulong_FF(dest,(unsigned int)10 * sizeof(unsigned long));
-  memset_ulong_FF(res,(unsigned int)10 * sizeof(unsigned long));
+    memset_ulong_FF(dest,(unsigned long)10 * sizeof(unsigned long));
+  memset_ulong_FF(res,(unsigned long)10 * sizeof(unsigned long));
   return;
 }
 
@@ -251,8 +252,8 @@ long long *memset_llong_FF(long long *ptr, size_t len)
 void long_long_integer(long long * /*[10]*/ dest)
 {
   long long *res =
-    memset_llong_FF(dest,(unsigned int)10 * sizeof(long long));
-  memset_llong_FF(res,(unsigned int)10 * sizeof(long long));
+    memset_llong_FF(dest,(unsigned long)10 * sizeof(long long));
+  memset_llong_FF(res,(unsigned long)10 * sizeof(long long));
   return;
 }
 
@@ -279,8 +280,8 @@ unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len)
 void unsigned_long_long_integer(unsigned long long * /*[10]*/ dest)
 {
   unsigned long long *res =
-    memset_ullong_FF(dest,(unsigned int)10 * sizeof(unsigned long long));
-  memset_ullong_FF(res,(unsigned int)10 * sizeof(unsigned long long));
+    memset_ullong_FF(dest,(unsigned long)10 * sizeof(unsigned long long));
+  memset_ullong_FF(res,(unsigned long)10 * sizeof(unsigned long long));
   return;
 }
 
@@ -305,15 +306,15 @@ float *memset_float_FF(float *ptr, size_t len)
 
 void floats(float * /*[10]*/ dest)
 {
-  float *res = memset_float_FF(dest,(unsigned int)10 * sizeof(float));
-  memset_float_FF(res,(unsigned int)10 * sizeof(float));
+  float *res = memset_float_FF(dest,(unsigned long)10 * sizeof(float));
+  memset_float_FF(res,(unsigned long)10 * sizeof(float));
   return;
 }
 
 void with_named(named * /*[10]*/ dest)
 {
-  named *res = memset_int_FF(dest,(unsigned int)10 * sizeof(named));
-  memset_int_FF(res,(unsigned int)10 * sizeof(named));
+  named *res = memset_int_FF(dest,(unsigned long)10 * sizeof(named));
+  memset_int_FF(res,(unsigned long)10 * sizeof(named));
   return;
 }
 
@@ -340,21 +341,21 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len)
 
 void structure(struct X * /*[10]*/ dest)
 {
-  struct X *res = memset_st_X_FF(dest,(unsigned int)10 * sizeof(struct X));
-  memset_st_X_FF(res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memset_st_X_FF(dest,(unsigned long)10 * sizeof(struct X));
+  memset_st_X_FF(res,(unsigned long)10 * sizeof(struct X));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
     ensures
       set_content:
-        \let __fc_len = len / 4;
+        \let __fc_len = len / 8;
         ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(ptr + j0));
     ensures result: \result ≡ ptr;
-    assigns *(ptr + (0 .. len / 4 - 1)), \result;
-    assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+    assigns *(ptr + (0 .. len / 8 - 1)), \result;
+    assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
     assigns \result \from ptr;
  */
 int **memset_ptr_int_FF(int **ptr, size_t len)
@@ -366,8 +367,8 @@ int **memset_ptr_int_FF(int **ptr, size_t len)
 
 void pointers(int ** /*[10]*/ dest)
 {
-  int **res = memset_ptr_int_FF(dest,(unsigned int)10 * sizeof(int *));
-  memset_ptr_int_FF(res,(unsigned int)10 * sizeof(int *));
+  int **res = memset_ptr_int_FF(dest,(unsigned long)10 * sizeof(int *));
+  memset_ptr_int_FF(res,(unsigned long)10 * sizeof(int *));
   return;
 }
 
@@ -395,22 +396,22 @@ int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10]
 void nested(int (*dest)[10], int n)
 {
   int (*res)[10] =
-    memset_arr10_int_FF(dest,(unsigned int)n * sizeof(int [10]));
-  memset_arr10_int_FF(res,(unsigned int)n * sizeof(int [10]));
+    memset_arr10_int_FF(dest,(unsigned long)n * sizeof(int [10]));
+  memset_arr10_int_FF(res,(unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *dest)
 {
-  void *res = memset(dest,0xFF,(unsigned int)10);
-  memset(res,0xFF,(unsigned int)10);
+  void *res = memset(dest,0xFF,(unsigned long)10);
+  memset(res,0xFF,(unsigned long)10);
   return;
 }
 
 void with_null_or_int(void)
 {
-  memset((void *)0,0xFF,(unsigned int)10);
-  memset((void *)((int *)42),0xFF,(unsigned int)10);
+  memset((void *)0,0xFF,(unsigned long)10);
+  memset((void *)((int *)42),0xFF,(unsigned long)10);
   return;
 }
 
@@ -450,8 +451,8 @@ char *memset_char(char *ptr, char value, size_t len)
 
 void chars(char *dest)
 {
-  char *res = memset_char(dest,(char)0xFF,(unsigned int)10);
-  memset_char(res,(char)0xFF,(unsigned int)10);
+  char *res = memset_char(dest,(char)0xFF,(unsigned long)10);
+  memset_char(res,(char)0xFF,(unsigned long)10);
   return;
 }
 
@@ -477,8 +478,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
 void uchars(unsigned char *dest)
 {
   unsigned char *res =
-    memset_uchar(dest,(unsigned char)0xFF,(unsigned int)10);
-  memset_uchar(res,(unsigned char)0xFF,(unsigned int)10);
+    memset_uchar(dest,(unsigned char)0xFF,(unsigned long)10);
+  memset_uchar(res,(unsigned char)0xFF,(unsigned long)10);
   return;
 }
 
@@ -506,8 +507,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
 
 void nested_chars(char (*dest)[10])
 {
-  char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned int)100);
-  memset_arr10_char(res,(char)0xFF,(unsigned int)100);
+  char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned long)100);
+  memset_arr10_char(res,(char)0xFF,(unsigned long)100);
   return;
 }
 
@@ -532,8 +533,8 @@ int *memset_int_FF(int *ptr, size_t len)
 
 void integer(int *dest)
 {
-  int *res = memset_int_FF(dest,(unsigned int)10 * sizeof(int));
-  memset_int_FF(res,(unsigned int)10 * sizeof(int));
+  int *res = memset_int_FF(dest,(unsigned long)10 * sizeof(int));
+  memset_int_FF(res,(unsigned long)10 * sizeof(int));
   return;
 }
 
@@ -558,8 +559,8 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len)
 
 void with_enum(enum E *dest)
 {
-  enum E *res = memset_e_E_FF(dest,(unsigned int)10 * sizeof(enum E));
-  memset_e_E_FF(res,(unsigned int)10 * sizeof(enum E));
+  enum E *res = memset_e_E_FF(dest,(unsigned long)10 * sizeof(enum E));
+  memset_e_E_FF(res,(unsigned long)10 * sizeof(enum E));
   return;
 }
 
@@ -585,21 +586,21 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
 void unsigned_integer(unsigned int *dest)
 {
   unsigned int *res =
-    memset_uint_FF(dest,(unsigned int)10 * sizeof(unsigned int));
-  memset_uint_FF(res,(unsigned int)10 * sizeof(unsigned int));
+    memset_uint_FF(dest,(unsigned long)10 * sizeof(unsigned int));
+  memset_uint_FF(res,(unsigned long)10 * sizeof(unsigned int));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
     ensures
       set_content:
-        \let __fc_len = \old(len) / 4;
+        \let __fc_len = \old(len) / 8;
         ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((long)0);
     ensures result: \result ≡ \old(ptr);
-    assigns *(ptr + (0 .. len / 4 - 1)), \result;
-    assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+    assigns *(ptr + (0 .. len / 8 - 1)), \result;
+    assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
     assigns \result \from ptr;
  */
 long *memset_long_FF(long *ptr, size_t len)
@@ -611,21 +612,22 @@ long *memset_long_FF(long *ptr, size_t len)
 
 void long_integer(long *dest)
 {
-  long *res = memset_long_FF(dest,(unsigned int)10 * sizeof(long));
-  memset_long_FF(res,(unsigned int)10 * sizeof(long));
+  long *res = memset_long_FF(dest,(unsigned long)10 * sizeof(long));
+  memset_long_FF(res,(unsigned long)10 * sizeof(long));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
     ensures
       set_content:
-        \let __fc_len = \old(len) / 4;
-        ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 4294967295;
+        \let __fc_len = \old(len) / 8;
+        ∀ ℤ j0;
+          0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 18446744073709551615;
     ensures result: \result ≡ \old(ptr);
-    assigns *(ptr + (0 .. len / 4 - 1)), \result;
-    assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+    assigns *(ptr + (0 .. len / 8 - 1)), \result;
+    assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
     assigns \result \from ptr;
  */
 unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
@@ -638,8 +640,8 @@ unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
 void unsigned_long_integer(unsigned long *dest)
 {
   unsigned long *res =
-    memset_ulong_FF(dest,(unsigned int)10 * sizeof(unsigned long));
-  memset_ulong_FF(res,(unsigned int)10 * sizeof(unsigned long));
+    memset_ulong_FF(dest,(unsigned long)10 * sizeof(unsigned long));
+  memset_ulong_FF(res,(unsigned long)10 * sizeof(unsigned long));
   return;
 }
 
@@ -666,8 +668,8 @@ long long *memset_llong_FF(long long *ptr, size_t len)
 void long_long_integer(long long *dest)
 {
   long long *res =
-    memset_llong_FF(dest,(unsigned int)10 * sizeof(long long));
-  memset_llong_FF(res,(unsigned int)10 * sizeof(long long));
+    memset_llong_FF(dest,(unsigned long)10 * sizeof(long long));
+  memset_llong_FF(res,(unsigned long)10 * sizeof(long long));
   return;
 }
 
@@ -694,8 +696,8 @@ unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len)
 void unsigned_long_long_integer(unsigned long long *dest)
 {
   unsigned long long *res =
-    memset_ullong_FF(dest,(unsigned int)10 * sizeof(unsigned long long));
-  memset_ullong_FF(res,(unsigned int)10 * sizeof(unsigned long long));
+    memset_ullong_FF(dest,(unsigned long)10 * sizeof(unsigned long long));
+  memset_ullong_FF(res,(unsigned long)10 * sizeof(unsigned long long));
   return;
 }
 
@@ -720,15 +722,15 @@ float *memset_float_FF(float *ptr, size_t len)
 
 void floats(float *dest)
 {
-  float *res = memset_float_FF(dest,(unsigned int)10 * sizeof(float));
-  memset_float_FF(res,(unsigned int)10 * sizeof(float));
+  float *res = memset_float_FF(dest,(unsigned long)10 * sizeof(float));
+  memset_float_FF(res,(unsigned long)10 * sizeof(float));
   return;
 }
 
 void with_named(named *dest)
 {
-  named *res = memset_int_FF(dest,(unsigned int)10 * sizeof(named));
-  memset_int_FF(res,(unsigned int)10 * sizeof(named));
+  named *res = memset_int_FF(dest,(unsigned long)10 * sizeof(named));
+  memset_int_FF(res,(unsigned long)10 * sizeof(named));
   return;
 }
 
@@ -756,21 +758,21 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len)
 
 void structure(struct X *dest)
 {
-  struct X *res = memset_st_X_FF(dest,(unsigned int)10 * sizeof(struct X));
-  memset_st_X_FF(res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memset_st_X_FF(dest,(unsigned long)10 * sizeof(struct X));
+  memset_st_X_FF(res,(unsigned long)10 * sizeof(struct X));
   return;
 }
 
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires aligned_end: len % 8 ≡ 0;
     requires
-      valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1));
+      valid_dest: \let __fc_len = len / 8; \valid(ptr + (0 .. __fc_len - 1));
     ensures
       set_content:
-        \let __fc_len = \old(len) / 4;
+        \let __fc_len = \old(len) / 8;
         ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(\old(ptr) + j0));
     ensures result: \result ≡ \old(ptr);
-    assigns *(ptr + (0 .. len / 4 - 1)), \result;
-    assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing;
+    assigns *(ptr + (0 .. len / 8 - 1)), \result;
+    assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
     assigns \result \from ptr;
  */
 int **memset_ptr_int_FF(int **ptr, size_t len)
@@ -782,8 +784,8 @@ int **memset_ptr_int_FF(int **ptr, size_t len)
 
 void pointers(int **dest)
 {
-  int **res = memset_ptr_int_FF(dest,(unsigned int)10 * sizeof(int *));
-  memset_ptr_int_FF(res,(unsigned int)10 * sizeof(int *));
+  int **res = memset_ptr_int_FF(dest,(unsigned long)10 * sizeof(int *));
+  memset_ptr_int_FF(res,(unsigned long)10 * sizeof(int *));
   return;
 }
 
@@ -812,22 +814,22 @@ int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10]
 void nested(int (*dest)[10], int n)
 {
   int (*res)[10] =
-    memset_arr10_int_FF(dest,(unsigned int)n * sizeof(int [10]));
-  memset_arr10_int_FF(res,(unsigned int)n * sizeof(int [10]));
+    memset_arr10_int_FF(dest,(unsigned long)n * sizeof(int [10]));
+  memset_arr10_int_FF(res,(unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *dest)
 {
-  void *res = memset(dest,0xFF,(unsigned int)10);
-  memset(res,0xFF,(unsigned int)10);
+  void *res = memset(dest,0xFF,(unsigned long)10);
+  memset(res,0xFF,(unsigned long)10);
   return;
 }
 
 void with_null_or_int(void)
 {
-  memset((void *)0,0xFF,(unsigned int)10);
-  memset((void *)((int *)42),0xFF,(unsigned int)10);
+  memset((void *)0,0xFF,(unsigned long)10);
+  memset((void *)((int *)42),0xFF,(unsigned long)10);
   return;
 }
 
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
index 5ece8370f6b..d355aff8a40 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
@@ -68,8 +68,8 @@ char *memset_char(char *ptr, char value, size_t len)
 
 void chars(char * /*[10]*/ dest, char value)
 {
-  char *res = memset_char(dest,value,(unsigned int)10);
-  memset_char(res,value,(unsigned int)10);
+  char *res = memset_char(dest,value,(unsigned long)10);
+  memset_char(res,value,(unsigned long)10);
   return;
 }
 
@@ -92,8 +92,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
 
 void uchars(char * /*[10]*/ dest, unsigned char value)
 {
-  unsigned char *res = memset_char(dest,(char)value,(unsigned int)10);
-  memset_uchar(res,value,(unsigned int)10);
+  unsigned char *res = memset_char(dest,(char)value,(unsigned long)10);
+  memset_uchar(res,value,(unsigned long)10);
   return;
 }
 
@@ -120,73 +120,74 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
 
 void nested_chars(char (* /*[10]*/ dest)[10], char value)
 {
-  char (*res)[10] = memset_arr10_char(dest,value,(unsigned int)100);
-  memset_arr10_char(res,value,(unsigned int)100);
+  char (*res)[10] = memset_arr10_char(dest,value,(unsigned long)100);
+  memset_arr10_char(res,value,(unsigned long)100);
   return;
 }
 
 void integer(int * /*[10]*/ dest, int value)
 {
-  int *res = memset((void *)dest,value,(unsigned int)10 * sizeof(int));
-  memset((void *)res,value,(unsigned int)10 * sizeof(int));
+  int *res = memset((void *)dest,value,(unsigned long)10 * sizeof(int));
+  memset((void *)res,value,(unsigned long)10 * sizeof(int));
   return;
 }
 
 void with_enum(enum E * /*[10]*/ dest, int value)
 {
-  enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E));
-  memset((void *)res,value,(unsigned int)10 * sizeof(enum E));
+  enum E *res =
+    memset((void *)dest,value,(unsigned long)10 * sizeof(enum E));
+  memset((void *)res,value,(unsigned long)10 * sizeof(enum E));
   return;
 }
 
 void with_named(named * /*[10]*/ dest, int value)
 {
-  named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named));
-  memset((void *)res,value,(unsigned int)10 * sizeof(named));
+  named *res = memset((void *)dest,value,(unsigned long)10 * sizeof(named));
+  memset((void *)res,value,(unsigned long)10 * sizeof(named));
   return;
 }
 
 void structure(struct X * /*[10]*/ dest, int value)
 {
   struct X *res =
-    memset((void *)dest,value,(unsigned int)10 * sizeof(struct X));
-  memset((void *)res,value,(unsigned int)10 * sizeof(struct X));
+    memset((void *)dest,value,(unsigned long)10 * sizeof(struct X));
+  memset((void *)res,value,(unsigned long)10 * sizeof(struct X));
   return;
 }
 
 void pointers(int ** /*[10]*/ dest, int value)
 {
-  int **res = memset((void *)dest,value,(unsigned int)10 * sizeof(int *));
-  memset((void *)res,value,(unsigned int)10 * sizeof(int *));
+  int **res = memset((void *)dest,value,(unsigned long)10 * sizeof(int *));
+  memset((void *)res,value,(unsigned long)10 * sizeof(int *));
   return;
 }
 
 void nested(int (*dest)[10], int n, int value)
 {
   int (*res)[10] =
-    memset((void *)dest,value,(unsigned int)n * sizeof(int [10]));
-  memset((void *)res,value,(unsigned int)n * sizeof(int [10]));
+    memset((void *)dest,value,(unsigned long)n * sizeof(int [10]));
+  memset((void *)res,value,(unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *dest, int value)
 {
-  void *res = memset(dest,value,(unsigned int)10);
-  memset(res,value,(unsigned int)10);
+  void *res = memset(dest,value,(unsigned long)10);
+  memset(res,value,(unsigned long)10);
   return;
 }
 
 void with_incomplete(struct incomplete *dest, int value)
 {
-  struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
-  memset((void *)res,value,(unsigned int)10);
+  struct incomplete *res = memset((void *)dest,value,(unsigned long)10);
+  memset((void *)res,value,(unsigned long)10);
   return;
 }
 
 void with_null_or_int(int value)
 {
-  memset((void *)0,value,(unsigned int)10);
-  memset((void *)((int *)42),value,(unsigned int)10);
+  memset((void *)0,value,(unsigned long)10);
+  memset((void *)((int *)42),value,(unsigned long)10);
   return;
 }
 
@@ -227,8 +228,8 @@ char *memset_char(char *ptr, char value, size_t len)
 
 void chars(char *dest, char value)
 {
-  char *res = memset_char(dest,value,(unsigned int)10);
-  memset_char(res,value,(unsigned int)10);
+  char *res = memset_char(dest,value,(unsigned long)10);
+  memset_char(res,value,(unsigned long)10);
   return;
 }
 
@@ -253,8 +254,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
 
 void uchars(char *dest, unsigned char value)
 {
-  unsigned char *res = memset_char(dest,(char)value,(unsigned int)10);
-  memset_uchar(res,value,(unsigned int)10);
+  unsigned char *res = memset_char(dest,(char)value,(unsigned long)10);
+  memset_uchar(res,value,(unsigned long)10);
   return;
 }
 
@@ -282,73 +283,74 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
 
 void nested_chars(char (*dest)[10], char value)
 {
-  char (*res)[10] = memset_arr10_char(dest,value,(unsigned int)100);
-  memset_arr10_char(res,value,(unsigned int)100);
+  char (*res)[10] = memset_arr10_char(dest,value,(unsigned long)100);
+  memset_arr10_char(res,value,(unsigned long)100);
   return;
 }
 
 void integer(int *dest, int value)
 {
-  int *res = memset((void *)dest,value,(unsigned int)10 * sizeof(int));
-  memset((void *)res,value,(unsigned int)10 * sizeof(int));
+  int *res = memset((void *)dest,value,(unsigned long)10 * sizeof(int));
+  memset((void *)res,value,(unsigned long)10 * sizeof(int));
   return;
 }
 
 void with_enum(enum E *dest, int value)
 {
-  enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E));
-  memset((void *)res,value,(unsigned int)10 * sizeof(enum E));
+  enum E *res =
+    memset((void *)dest,value,(unsigned long)10 * sizeof(enum E));
+  memset((void *)res,value,(unsigned long)10 * sizeof(enum E));
   return;
 }
 
 void with_named(named *dest, int value)
 {
-  named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named));
-  memset((void *)res,value,(unsigned int)10 * sizeof(named));
+  named *res = memset((void *)dest,value,(unsigned long)10 * sizeof(named));
+  memset((void *)res,value,(unsigned long)10 * sizeof(named));
   return;
 }
 
 void structure(struct X *dest, int value)
 {
   struct X *res =
-    memset((void *)dest,value,(unsigned int)10 * sizeof(struct X));
-  memset((void *)res,value,(unsigned int)10 * sizeof(struct X));
+    memset((void *)dest,value,(unsigned long)10 * sizeof(struct X));
+  memset((void *)res,value,(unsigned long)10 * sizeof(struct X));
   return;
 }
 
 void pointers(int **dest, int value)
 {
-  int **res = memset((void *)dest,value,(unsigned int)10 * sizeof(int *));
-  memset((void *)res,value,(unsigned int)10 * sizeof(int *));
+  int **res = memset((void *)dest,value,(unsigned long)10 * sizeof(int *));
+  memset((void *)res,value,(unsigned long)10 * sizeof(int *));
   return;
 }
 
 void nested(int (*dest)[10], int n, int value)
 {
   int (*res)[10] =
-    memset((void *)dest,value,(unsigned int)n * sizeof(int [10]));
-  memset((void *)res,value,(unsigned int)n * sizeof(int [10]));
+    memset((void *)dest,value,(unsigned long)n * sizeof(int [10]));
+  memset((void *)res,value,(unsigned long)n * sizeof(int [10]));
   return;
 }
 
 void with_void(void *dest, int value)
 {
-  void *res = memset(dest,value,(unsigned int)10);
-  memset(res,value,(unsigned int)10);
+  void *res = memset(dest,value,(unsigned long)10);
+  memset(res,value,(unsigned long)10);
   return;
 }
 
 void with_incomplete(struct incomplete *dest, int value)
 {
-  struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
-  memset((void *)res,value,(unsigned int)10);
+  struct incomplete *res = memset((void *)dest,value,(unsigned long)10);
+  memset((void *)res,value,(unsigned long)10);
   return;
 }
 
 void with_null_or_int(int value)
 {
-  memset((void *)0,value,(unsigned int)10);
-  memset((void *)((int *)42),value,(unsigned int)10);
+  memset((void *)0,value,(unsigned long)10);
+  memset((void *)((int *)42),value,(unsigned long)10);
   return;
 }
 
-- 
GitLab