From 79e08809e12f1d3562b3b29b2256d88074ce5b44 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 30 Mar 2021 16:29:10 +0200
Subject: [PATCH] [tests] update oracles

---
 .../tests/string/oracle/memcmp.res.oracle     | 20 +++----
 .../tests/string/oracle/memcpy.res.oracle     | 20 +++----
 .../tests/string/oracle/memmove.res.oracle    | 20 +++----
 .../tests/string/oracle/memset_0.res.oracle   | 36 ++++++------
 .../tests/string/oracle/memset_FF.res.oracle  | 56 +++++++++----------
 .../string/oracle/memset_value.res.oracle     | 32 +++++------
 .../wp_acsl/oracle/chunk_typing.res.oracle    |  7 +--
 tests/libc/oracle/fc_libc.1.res.oracle        | 20 +++----
 tests/rte/oracle/tab.res.oracle               |  2 +-
 tests/spec/oracle/array_conversion.res.oracle |  2 +-
 tests/spec/oracle/array_typedef.res.oracle    |  4 +-
 tests/spec/oracle/range.res.oracle            |  2 +-
 tests/spec/oracle/rm_qualifiers.res.oracle    |  2 +-
 tests/spec/oracle/tsets.res.oracle            |  2 +-
 tests/syntax/oracle/assembly_gmp.0.res.oracle |  2 +-
 tests/syntax/oracle/assembly_gmp.1.res.oracle |  2 +-
 tests/syntax/oracle/assembly_gmp.2.res.oracle |  2 +-
 tests/syntax/oracle/bts0519.0.res.oracle      |  2 +-
 .../oracle/dangerous_expressions.res.oracle   |  2 +-
 .../syntax/oracle/enum_size_array.res.oracle  |  2 +-
 tests/value/oracle/assigns.res.oracle         |  2 +-
 21 files changed, 119 insertions(+), 120 deletions(-)

diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
index dd2862c8e5f..7923384e2ab 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
@@ -45,14 +45,14 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
   return __retres;
 }
 
-int integer(int * /*[10]*/ s1, int * /*[10]*/ s2)
+int integer(int s1[10], int s2[10])
 {
   int tmp;
   tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(int));
   return tmp;
 }
 
-int with_named(named * /*[10]*/ s1, named * /*[10]*/ s2)
+int with_named(named s1[10], named s2[10])
 {
   int tmp;
   tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(named));
@@ -83,7 +83,7 @@ int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
   return __retres;
 }
 
-int structure(struct X * /*[10]*/ s1, struct X * /*[10]*/ s2)
+int structure(struct X s1[10], struct X s2[10])
 {
   int tmp;
   tmp = memcmp_st_X(s1,s2,(unsigned long)10 * sizeof(struct X));
@@ -114,7 +114,7 @@ int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
   return __retres;
 }
 
-int pointers(int ** /*[10]*/ s1, int ** /*[10]*/ s2)
+int pointers(int *s1[10], int *s2[10])
 {
   int tmp;
   tmp = memcmp_ptr_int(s1,s2,(unsigned long)10 * sizeof(int *));
@@ -169,7 +169,7 @@ int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
   return tmp;
 }
 
-void with_null_or_int(int * /*[10]*/ p)
+void with_null_or_int(int p[10])
 {
   memcmp((void const *)0,(void const *)p,(unsigned long)10 * sizeof(int));
   memcmp((void const *)p,(void const *)0,(unsigned long)10 * sizeof(int));
@@ -217,7 +217,7 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
   return __retres;
 }
 
-int integer(int *s1, int *s2)
+int integer(int s1[10], int s2[10])
 {
   int tmp;
   tmp = memcmp_int((int const *)s1,(int const *)s2,
@@ -225,7 +225,7 @@ int integer(int *s1, int *s2)
   return tmp;
 }
 
-int with_named(named *s1, named *s2)
+int with_named(named s1[10], named s2[10])
 {
   int tmp;
   tmp = memcmp_int((int const *)s1,(int const *)s2,
@@ -258,7 +258,7 @@ int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
   return __retres;
 }
 
-int structure(struct X *s1, struct X *s2)
+int structure(struct X s1[10], struct X s2[10])
 {
   int tmp;
   tmp = memcmp_st_X((struct X const *)s1,(struct X const *)s2,
@@ -291,7 +291,7 @@ int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
   return __retres;
 }
 
-int pointers(int **s1, int **s2)
+int pointers(int *s1[10], int *s2[10])
 {
   int tmp;
   tmp = memcmp_ptr_int((int * const *)s1,(int * const *)s2,
@@ -349,7 +349,7 @@ int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
   return tmp;
 }
 
-void with_null_or_int(int *p)
+void with_null_or_int(int p[10])
 {
   memcmp((void const *)0,(void const *)p,(unsigned long)10 * sizeof(int));
   memcmp((void const *)p,(void const *)0,(unsigned long)10 * sizeof(int));
diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 259a1cacb16..994ecf23048 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
@@ -51,14 +51,14 @@ int *memcpy_int(int *dest, int const *src, size_t len)
   return __retres;
 }
 
-void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
+void integer(int src[10], int dest[10])
 {
   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)
+void with_named(named src[10], named dest[10])
 {
   named *res = memcpy_int(dest,src,(unsigned long)10 * sizeof(named));
   memcpy_int(src,res,(unsigned long)10 * sizeof(named));
@@ -91,7 +91,7 @@ struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
   return __retres;
 }
 
-void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
+void structure(struct X src[10], struct X dest[10])
 {
   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));
@@ -124,7 +124,7 @@ int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
   return __retres;
 }
 
-void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
+void pointers(int *src[10], int *dest[10])
 {
   int **res = memcpy_ptr_int(dest,src,(unsigned long)10 * sizeof(int *));
   memcpy_ptr_int(src,res,(unsigned long)10 * sizeof(int *));
@@ -185,7 +185,7 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
   return;
 }
 
-void with_null_or_int(int * /*[10]*/ p)
+void with_null_or_int(int p[10])
 {
   memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
   memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
@@ -233,7 +233,7 @@ int *memcpy_int(int *dest, int const *src, size_t len)
   return __retres;
 }
 
-void integer(int *src, int *dest)
+void integer(int src[10], int dest[10])
 {
   int *res =
     memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(int));
@@ -241,7 +241,7 @@ void integer(int *src, int *dest)
   return;
 }
 
-void with_named(named *src, named *dest)
+void with_named(named src[10], named dest[10])
 {
   named *res =
     memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(named));
@@ -276,7 +276,7 @@ struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
   return __retres;
 }
 
-void structure(struct X *src, struct X *dest)
+void structure(struct X src[10], struct X dest[10])
 {
   struct X *res =
     memcpy_st_X(dest,(struct X const *)src,
@@ -312,7 +312,7 @@ int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
   return __retres;
 }
 
-void pointers(int **src, int **dest)
+void pointers(int *src[10], int *dest[10])
 {
   int **res =
     memcpy_ptr_int(dest,(int * const *)src,(unsigned long)10 * sizeof(int *));
@@ -377,7 +377,7 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
   return;
 }
 
-void with_null_or_int(int *p)
+void with_null_or_int(int p[10])
 {
   memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
   memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
index fc4bf692213..660db18e3fa 100644
--- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
@@ -47,14 +47,14 @@ int *memmove_int(int *dest, int const *src, size_t len)
   return __retres;
 }
 
-void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
+void integer(int src[10], int dest[10])
 {
   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)
+void with_named(named src[10], named dest[10])
 {
   named *res = memmove_int(dest,src,(unsigned long)10 * sizeof(named));
   memmove_int(src,res,(unsigned long)10 * sizeof(named));
@@ -83,7 +83,7 @@ struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
   return __retres;
 }
 
-void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
+void structure(struct X src[10], struct X dest[10])
 {
   struct X *res =
     memmove_st_X(dest,src,(unsigned long)10 * sizeof(struct X));
@@ -113,7 +113,7 @@ int **memmove_ptr_int(int **dest, int * const *src, size_t len)
   return __retres;
 }
 
-void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
+void pointers(int *src[10], int *dest[10])
 {
   int **res = memmove_ptr_int(dest,src,(unsigned long)10 * sizeof(int *));
   memmove_ptr_int(src,res,(unsigned long)10 * sizeof(int *));
@@ -170,7 +170,7 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
   return;
 }
 
-void with_null_or_int(int * /*[10]*/ p)
+void with_null_or_int(int p[10])
 {
   memmove((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
   memmove((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
@@ -216,7 +216,7 @@ int *memmove_int(int *dest, int const *src, size_t len)
   return __retres;
 }
 
-void integer(int *src, int *dest)
+void integer(int src[10], int dest[10])
 {
   int *res =
     memmove_int(dest,(int const *)src,(unsigned long)10 * sizeof(int));
@@ -224,7 +224,7 @@ void integer(int *src, int *dest)
   return;
 }
 
-void with_named(named *src, named *dest)
+void with_named(named src[10], named dest[10])
 {
   named *res =
     memmove_int(dest,(int const *)src,(unsigned long)10 * sizeof(named));
@@ -255,7 +255,7 @@ struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
   return __retres;
 }
 
-void structure(struct X *src, struct X *dest)
+void structure(struct X src[10], struct X dest[10])
 {
   struct X *res =
     memmove_st_X(dest,(struct X const *)src,
@@ -288,7 +288,7 @@ int **memmove_ptr_int(int **dest, int * const *src, size_t len)
   return __retres;
 }
 
-void pointers(int **src, int **dest)
+void pointers(int *src[10], int *dest[10])
 {
   int **res =
     memmove_ptr_int(dest,(int * const *)src,
@@ -350,7 +350,7 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
   return;
 }
 
-void with_null_or_int(int *p)
+void with_null_or_int(int p[10])
 {
   memmove((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
   memmove((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
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 f0925319e77..e38819902b0 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
@@ -37,7 +37,7 @@ char *memset_char(char *ptr, char value, size_t len)
   return __retres;
 }
 
-void chars(char * /*[10]*/ dest)
+void chars(char dest[10])
 {
   char *res = memset_char(dest,(char)0,(unsigned long)10);
   memset_char(res,(char)0,(unsigned long)10);
@@ -61,7 +61,7 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
   return __retres;
 }
 
-void uchars(unsigned char * /*[10]*/ dest)
+void uchars(unsigned char dest[10])
 {
   unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned long)10);
   memset_uchar(res,(unsigned char)0,(unsigned long)10);
@@ -89,7 +89,7 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
   return __retres;
 }
 
-void nested_chars(char (* /*[10]*/ dest)[10])
+void nested_chars(char dest[10][10])
 {
   char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned long)100);
   memset_arr10_char(res,(char)0,(unsigned long)100);
@@ -115,7 +115,7 @@ int *memset_int_0(int *ptr, size_t len)
   return __retres;
 }
 
-void integer(int * /*[10]*/ dest)
+void integer(int dest[10])
 {
   int *res = memset_int_0(dest,(unsigned long)10 * sizeof(int));
   memset_int_0(res,(unsigned long)10 * sizeof(int));
@@ -141,7 +141,7 @@ enum E *memset_e_E_0(enum E *ptr, size_t len)
   return __retres;
 }
 
-void with_enum(enum E * /*[10]*/ dest)
+void with_enum(enum E dest[10])
 {
   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));
@@ -167,14 +167,14 @@ float *memset_float_0(float *ptr, size_t len)
   return __retres;
 }
 
-void floats(float * /*[10]*/ dest)
+void floats(float dest[10])
 {
   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)
+void with_named(named dest[10])
 {
   named *res = memset_int_0(dest,(unsigned long)10 * sizeof(named));
   memset_int_0(res,(unsigned long)10 * sizeof(named));
@@ -201,7 +201,7 @@ struct X *memset_st_X_0(struct X *ptr, size_t len)
   return __retres;
 }
 
-void structure(struct X * /*[10]*/ dest)
+void structure(struct X dest[10])
 {
   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));
@@ -227,7 +227,7 @@ int **memset_ptr_int_0(int **ptr, size_t len)
   return __retres;
 }
 
-void pointers(int ** /*[10]*/ dest)
+void pointers(int *dest[10])
 {
   int **res = memset_ptr_int_0(dest,(unsigned long)10 * sizeof(int *));
   memset_ptr_int_0(res,(unsigned long)10 * sizeof(int *));
@@ -311,7 +311,7 @@ char *memset_char(char *ptr, char value, size_t len)
   return __retres;
 }
 
-void chars(char *dest)
+void chars(char dest[10])
 {
   char *res = memset_char(dest,(char)0,(unsigned long)10);
   memset_char(res,(char)0,(unsigned long)10);
@@ -337,7 +337,7 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
   return __retres;
 }
 
-void uchars(unsigned char *dest)
+void uchars(unsigned char dest[10])
 {
   unsigned char *res = memset_uchar(dest,(unsigned char)0,(unsigned long)10);
   memset_uchar(res,(unsigned char)0,(unsigned long)10);
@@ -366,7 +366,7 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
   return __retres;
 }
 
-void nested_chars(char (*dest)[10])
+void nested_chars(char dest[10][10])
 {
   char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned long)100);
   memset_arr10_char(res,(char)0,(unsigned long)100);
@@ -392,7 +392,7 @@ int *memset_int_0(int *ptr, size_t len)
   return __retres;
 }
 
-void integer(int *dest)
+void integer(int dest[10])
 {
   int *res = memset_int_0(dest,(unsigned long)10 * sizeof(int));
   memset_int_0(res,(unsigned long)10 * sizeof(int));
@@ -418,7 +418,7 @@ enum E *memset_e_E_0(enum E *ptr, size_t len)
   return __retres;
 }
 
-void with_enum(enum E *dest)
+void with_enum(enum E dest[10])
 {
   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));
@@ -444,14 +444,14 @@ float *memset_float_0(float *ptr, size_t len)
   return __retres;
 }
 
-void floats(float *dest)
+void floats(float dest[10])
 {
   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)
+void with_named(named dest[10])
 {
   named *res = memset_int_0(dest,(unsigned long)10 * sizeof(named));
   memset_int_0(res,(unsigned long)10 * sizeof(named));
@@ -479,7 +479,7 @@ struct X *memset_st_X_0(struct X *ptr, size_t len)
   return __retres;
 }
 
-void structure(struct X *dest)
+void structure(struct X dest[10])
 {
   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));
@@ -505,7 +505,7 @@ int **memset_ptr_int_0(int **ptr, size_t len)
   return __retres;
 }
 
-void pointers(int **dest)
+void pointers(int *dest[10])
 {
   int **res = memset_ptr_int_0(dest,(unsigned long)10 * sizeof(int *));
   memset_ptr_int_0(res,(unsigned long)10 * sizeof(int *));
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 798296c18a9..ba73c933112 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -37,7 +37,7 @@ char *memset_char(char *ptr, char value, size_t len)
   return __retres;
 }
 
-void chars(char * /*[10]*/ dest)
+void chars(char dest[10])
 {
   char *res = memset_char(dest,(char)0xFF,(unsigned long)10);
   memset_char(res,(char)0xFF,(unsigned long)10);
@@ -61,7 +61,7 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
   return __retres;
 }
 
-void uchars(unsigned char * /*[10]*/ dest)
+void uchars(unsigned char dest[10])
 {
   unsigned char *res =
     memset_uchar(dest,(unsigned char)0xFF,(unsigned long)10);
@@ -90,7 +90,7 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
   return __retres;
 }
 
-void nested_chars(char (* /*[10]*/ dest)[10])
+void nested_chars(char dest[10][10])
 {
   char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned long)100);
   memset_arr10_char(res,(char)0xFF,(unsigned long)100);
@@ -116,7 +116,7 @@ int *memset_int_FF(int *ptr, size_t len)
   return __retres;
 }
 
-void integer(int * /*[10]*/ dest)
+void integer(int dest[10])
 {
   int *res = memset_int_FF(dest,(unsigned long)10 * sizeof(int));
   memset_int_FF(res,(unsigned long)10 * sizeof(int));
@@ -142,7 +142,7 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len)
   return __retres;
 }
 
-void with_enum(enum E * /*[10]*/ dest)
+void with_enum(enum E dest[10])
 {
   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));
@@ -168,7 +168,7 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
   return __retres;
 }
 
-void unsigned_integer(unsigned int * /*[10]*/ dest)
+void unsigned_integer(unsigned int dest[10])
 {
   unsigned int *res =
     memset_uint_FF(dest,(unsigned long)10 * sizeof(unsigned int));
@@ -195,7 +195,7 @@ long *memset_long_FF(long *ptr, size_t len)
   return __retres;
 }
 
-void long_integer(long * /*[10]*/ dest)
+void long_integer(long dest[10])
 {
   long *res = memset_long_FF(dest,(unsigned long)10 * sizeof(long));
   memset_long_FF(res,(unsigned long)10 * sizeof(long));
@@ -222,7 +222,7 @@ unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
   return __retres;
 }
 
-void unsigned_long_integer(unsigned long * /*[10]*/ dest)
+void unsigned_long_integer(unsigned long dest[10])
 {
   unsigned long *res =
     memset_ulong_FF(dest,(unsigned long)10 * sizeof(unsigned long));
@@ -249,7 +249,7 @@ long long *memset_llong_FF(long long *ptr, size_t len)
   return __retres;
 }
 
-void long_long_integer(long long * /*[10]*/ dest)
+void long_long_integer(long long dest[10])
 {
   long long *res =
     memset_llong_FF(dest,(unsigned long)10 * sizeof(long long));
@@ -277,7 +277,7 @@ unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len)
   return __retres;
 }
 
-void unsigned_long_long_integer(unsigned long long * /*[10]*/ dest)
+void unsigned_long_long_integer(unsigned long long dest[10])
 {
   unsigned long long *res =
     memset_ullong_FF(dest,(unsigned long)10 * sizeof(unsigned long long));
@@ -304,14 +304,14 @@ float *memset_float_FF(float *ptr, size_t len)
   return __retres;
 }
 
-void floats(float * /*[10]*/ dest)
+void floats(float dest[10])
 {
   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)
+void with_named(named dest[10])
 {
   named *res = memset_int_FF(dest,(unsigned long)10 * sizeof(named));
   memset_int_FF(res,(unsigned long)10 * sizeof(named));
@@ -339,7 +339,7 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len)
   return __retres;
 }
 
-void structure(struct X * /*[10]*/ dest)
+void structure(struct X dest[10])
 {
   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));
@@ -365,7 +365,7 @@ int **memset_ptr_int_FF(int **ptr, size_t len)
   return __retres;
 }
 
-void pointers(int ** /*[10]*/ dest)
+void pointers(int *dest[10])
 {
   int **res = memset_ptr_int_FF(dest,(unsigned long)10 * sizeof(int *));
   memset_ptr_int_FF(res,(unsigned long)10 * sizeof(int *));
@@ -449,7 +449,7 @@ char *memset_char(char *ptr, char value, size_t len)
   return __retres;
 }
 
-void chars(char *dest)
+void chars(char dest[10])
 {
   char *res = memset_char(dest,(char)0xFF,(unsigned long)10);
   memset_char(res,(char)0xFF,(unsigned long)10);
@@ -475,7 +475,7 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
   return __retres;
 }
 
-void uchars(unsigned char *dest)
+void uchars(unsigned char dest[10])
 {
   unsigned char *res =
     memset_uchar(dest,(unsigned char)0xFF,(unsigned long)10);
@@ -505,7 +505,7 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
   return __retres;
 }
 
-void nested_chars(char (*dest)[10])
+void nested_chars(char dest[10][10])
 {
   char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned long)100);
   memset_arr10_char(res,(char)0xFF,(unsigned long)100);
@@ -531,7 +531,7 @@ int *memset_int_FF(int *ptr, size_t len)
   return __retres;
 }
 
-void integer(int *dest)
+void integer(int dest[10])
 {
   int *res = memset_int_FF(dest,(unsigned long)10 * sizeof(int));
   memset_int_FF(res,(unsigned long)10 * sizeof(int));
@@ -557,7 +557,7 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len)
   return __retres;
 }
 
-void with_enum(enum E *dest)
+void with_enum(enum E dest[10])
 {
   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));
@@ -583,7 +583,7 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
   return __retres;
 }
 
-void unsigned_integer(unsigned int *dest)
+void unsigned_integer(unsigned int dest[10])
 {
   unsigned int *res =
     memset_uint_FF(dest,(unsigned long)10 * sizeof(unsigned int));
@@ -610,7 +610,7 @@ long *memset_long_FF(long *ptr, size_t len)
   return __retres;
 }
 
-void long_integer(long *dest)
+void long_integer(long dest[10])
 {
   long *res = memset_long_FF(dest,(unsigned long)10 * sizeof(long));
   memset_long_FF(res,(unsigned long)10 * sizeof(long));
@@ -637,7 +637,7 @@ unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
   return __retres;
 }
 
-void unsigned_long_integer(unsigned long *dest)
+void unsigned_long_integer(unsigned long dest[10])
 {
   unsigned long *res =
     memset_ulong_FF(dest,(unsigned long)10 * sizeof(unsigned long));
@@ -665,7 +665,7 @@ long long *memset_llong_FF(long long *ptr, size_t len)
   return __retres;
 }
 
-void long_long_integer(long long *dest)
+void long_long_integer(long long dest[10])
 {
   long long *res =
     memset_llong_FF(dest,(unsigned long)10 * sizeof(long long));
@@ -693,7 +693,7 @@ unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len)
   return __retres;
 }
 
-void unsigned_long_long_integer(unsigned long long *dest)
+void unsigned_long_long_integer(unsigned long long dest[10])
 {
   unsigned long long *res =
     memset_ullong_FF(dest,(unsigned long)10 * sizeof(unsigned long long));
@@ -720,14 +720,14 @@ float *memset_float_FF(float *ptr, size_t len)
   return __retres;
 }
 
-void floats(float *dest)
+void floats(float dest[10])
 {
   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)
+void with_named(named dest[10])
 {
   named *res = memset_int_FF(dest,(unsigned long)10 * sizeof(named));
   memset_int_FF(res,(unsigned long)10 * sizeof(named));
@@ -756,7 +756,7 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len)
   return __retres;
 }
 
-void structure(struct X *dest)
+void structure(struct X dest[10])
 {
   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));
@@ -782,7 +782,7 @@ int **memset_ptr_int_FF(int **ptr, size_t len)
   return __retres;
 }
 
-void pointers(int **dest)
+void pointers(int *dest[10])
 {
   int **res = memset_ptr_int_FF(dest,(unsigned long)10 * sizeof(int *));
   memset_ptr_int_FF(res,(unsigned long)10 * sizeof(int *));
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 d355aff8a40..545f2fa144a 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
@@ -66,7 +66,7 @@ char *memset_char(char *ptr, char value, size_t len)
   return __retres;
 }
 
-void chars(char * /*[10]*/ dest, char value)
+void chars(char dest[10], char value)
 {
   char *res = memset_char(dest,value,(unsigned long)10);
   memset_char(res,value,(unsigned long)10);
@@ -90,7 +90,7 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
   return __retres;
 }
 
-void uchars(char * /*[10]*/ dest, unsigned char value)
+void uchars(char dest[10], unsigned char value)
 {
   unsigned char *res = memset_char(dest,(char)value,(unsigned long)10);
   memset_uchar(res,value,(unsigned long)10);
@@ -118,21 +118,21 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
   return __retres;
 }
 
-void nested_chars(char (* /*[10]*/ dest)[10], char value)
+void nested_chars(char dest[10][10], char value)
 {
   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)
+void integer(int dest[10], int value)
 {
   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)
+void with_enum(enum E dest[10], int value)
 {
   enum E *res =
     memset((void *)dest,value,(unsigned long)10 * sizeof(enum E));
@@ -140,14 +140,14 @@ void with_enum(enum E * /*[10]*/ dest, int value)
   return;
 }
 
-void with_named(named * /*[10]*/ dest, int value)
+void with_named(named dest[10], int value)
 {
   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)
+void structure(struct X dest[10], int value)
 {
   struct X *res =
     memset((void *)dest,value,(unsigned long)10 * sizeof(struct X));
@@ -155,7 +155,7 @@ void structure(struct X * /*[10]*/ dest, int value)
   return;
 }
 
-void pointers(int ** /*[10]*/ dest, int value)
+void pointers(int *dest[10], int value)
 {
   int **res = memset((void *)dest,value,(unsigned long)10 * sizeof(int *));
   memset((void *)res,value,(unsigned long)10 * sizeof(int *));
@@ -226,7 +226,7 @@ char *memset_char(char *ptr, char value, size_t len)
   return __retres;
 }
 
-void chars(char *dest, char value)
+void chars(char dest[10], char value)
 {
   char *res = memset_char(dest,value,(unsigned long)10);
   memset_char(res,value,(unsigned long)10);
@@ -252,7 +252,7 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
   return __retres;
 }
 
-void uchars(char *dest, unsigned char value)
+void uchars(char dest[10], unsigned char value)
 {
   unsigned char *res = memset_char(dest,(char)value,(unsigned long)10);
   memset_uchar(res,value,(unsigned long)10);
@@ -281,21 +281,21 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
   return __retres;
 }
 
-void nested_chars(char (*dest)[10], char value)
+void nested_chars(char dest[10][10], char value)
 {
   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)
+void integer(int dest[10], int value)
 {
   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)
+void with_enum(enum E dest[10], int value)
 {
   enum E *res =
     memset((void *)dest,value,(unsigned long)10 * sizeof(enum E));
@@ -303,14 +303,14 @@ void with_enum(enum E *dest, int value)
   return;
 }
 
-void with_named(named *dest, int value)
+void with_named(named dest[10], int value)
 {
   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)
+void structure(struct X dest[10], int value)
 {
   struct X *res =
     memset((void *)dest,value,(unsigned long)10 * sizeof(struct X));
@@ -318,7 +318,7 @@ void structure(struct X *dest, int value)
   return;
 }
 
-void pointers(int **dest, int value)
+void pointers(int *dest[10], int value)
 {
   int **res = memset((void *)dest,value,(unsigned long)10 * sizeof(int *));
   memset((void *)res,value,(unsigned long)10 * sizeof(int *));
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index e139ffdc57f..9455596589a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -1889,7 +1889,6 @@ Prove: true.
        requires \separated(u64 + (..), (char const *)x + (..));
        requires \separated(u8 + (..), (char const *)x + (..));
      */
-  void function(signed char * /*[10]*/ i8, unsigned char * /*[10]*/ u8,
-                short * /*[10]*/ i16, unsigned short * /*[10]*/ u16,
-                int * /*[10]*/ i32, unsigned int * /*[10]*/ u32,
-                long long * /*[10]*/ i64, unsigned long long * /*[10]*/ u64);
+  void function(signed char i8[10], unsigned char u8[10], short i16[10],
+                unsigned short u16[10], int i32[10], unsigned int u32[10],
+                long long i64[10], unsigned long long u64[10]);
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8390d1842cf..f3cd10d4f63 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1675,7 +1675,7 @@ extern long pathconf(char const *path, int name);
     assigns *(pipefd + (0 .. 1)) \from (indirect: __fc_fds[0 ..]);
     assigns \result \from (indirect: __fc_fds[0 ..]);
  */
-extern int pipe(int * /*[2]*/ pipefd);
+extern int pipe(int pipefd[2]);
 
 /*@ requires valid_fd: 0 ≤ fd < 1024;
     requires buf_has_room: \valid((char *)buf + (0 .. count - 1));
@@ -2221,14 +2221,14 @@ extern void srand48(long seed);
     assigns __fc_random48_init \from \nothing;
     assigns \result \from __fc_p_random48_counter;
  */
-extern unsigned short *seed48(unsigned short * /*[3]*/ seed16v);
+extern unsigned short *seed48(unsigned short seed16v[3]);
 
 /*@ ensures random48_initialized: __fc_random48_init ≡ 1;
     assigns __fc_random48_counter[0 .. 2], __fc_random48_init;
     assigns __fc_random48_counter[0 .. 2] \from *(param + (0 .. 5));
     assigns __fc_random48_init \from \nothing;
  */
-extern void lcong48(unsigned short * /*[7]*/ param);
+extern void lcong48(unsigned short param[7]);
 
 /*@ requires random48_initialized: __fc_random48_init ≡ 1;
     ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0;
@@ -2247,7 +2247,7 @@ extern double drand48(void);
       \from __fc_random48_counter[0 .. 2];
     assigns \result \from __fc_random48_counter[0 .. 2];
  */
-extern double erand48(unsigned short * /*[3]*/ xsubi);
+extern double erand48(unsigned short xsubi[3]);
 
 /*@ requires random48_initialized: __fc_random48_init ≡ 1;
     ensures result_range: 0 ≤ \result < 2147483648;
@@ -2266,7 +2266,7 @@ extern long lrand48(void);
       \from __fc_random48_counter[0 .. 2];
     assigns \result \from __fc_random48_counter[0 .. 2];
  */
-extern long nrand48(unsigned short * /*[3]*/ xsubi);
+extern long nrand48(unsigned short xsubi[3]);
 
 /*@ requires random48_initialized: __fc_random48_init ≡ 1;
     ensures result_range: -2147483648 ≤ \result < 2147483648;
@@ -2285,7 +2285,7 @@ extern long mrand48(void);
       \from __fc_random48_counter[0 .. 2];
     assigns \result \from __fc_random48_counter[0 .. 2];
  */
-extern long jrand48(unsigned short * /*[3]*/ xsubi);
+extern long jrand48(unsigned short xsubi[3]);
 
 void *calloc(size_t nmemb, size_t size);
 
@@ -3885,7 +3885,7 @@ extern int socket(int domain, int type, int protocol);
     assigns __fc_socket_counter \from __fc_socket_counter;
     assigns *(sv + (0 .. 1)) \from __fc_socket_counter;
  */
-extern int socketpair(int domain, int type, int protocol, int * /*[2]*/ sv);
+extern int socketpair(int domain, int type, int protocol, int sv[2]);
 
 struct in6_addr const in6addr_any = {.s6_addr = {(unsigned char)0}};
 struct in6_addr const in6addr_loopback =
@@ -7506,7 +7506,7 @@ extern int __va_openat_mode_t(int dirfd, char const *filename, int flags,
       \from (indirect: *(path + (0 .. strlen{Old}(path)))),
             (indirect: times), (indirect: *(times + (0 .. 1)));
  */
-extern int utimes(char const *path, struct timeval const * /*[2]*/ times);
+extern int utimes(char const *path, struct timeval const times[2]);
 
 /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result;
@@ -8031,11 +8031,11 @@ extern struct passwd *getpwnam(char const *name);
 extern struct passwd *getpwuid(uid_t uid);
 
 /*@ assigns *(env + (0 .. 4)); */
-extern int setjmp(int * /*[5]*/ env);
+extern int setjmp(int env[5]);
 
 /*@ ensures never_terminates: \false;
     assigns \nothing; */
-extern void longjmp(int * /*[5]*/ env, int val);
+extern void longjmp(int env[5], int val);
 
 /*@ ensures never_terminates: \false;
     assigns \nothing; */
diff --git a/tests/rte/oracle/tab.res.oracle b/tests/rte/oracle/tab.res.oracle
index 8e702b93806..15020c1bad8 100644
--- a/tests/rte/oracle/tab.res.oracle
+++ b/tests/rte/oracle/tab.res.oracle
@@ -14,7 +14,7 @@ double g4(typetab *t)
   return y;
 }
 
-double h4(double * /*[2]*/ t)
+double h4(double t[2])
 {
   double __retres;
   /*@ assert rte: mem_access: \valid_read(t + 0); */
diff --git a/tests/spec/oracle/array_conversion.res.oracle b/tests/spec/oracle/array_conversion.res.oracle
index a6d94451ed9..d502027cdad 100644
--- a/tests/spec/oracle/array_conversion.res.oracle
+++ b/tests/spec/oracle/array_conversion.res.oracle
@@ -17,7 +17,7 @@ foo X = {0, 1, 2, 3};
 /*@ lemma vaddrof2{L}: \valid((int *)X);
  */
 /*@ requires p1(x); */
-int f1(int * /*[4]*/ x)
+int f1(int x[4])
 {
   int __retres;
   __retres = *(x + 3);
diff --git a/tests/spec/oracle/array_typedef.res.oracle b/tests/spec/oracle/array_typedef.res.oracle
index 51da3e81b84..0175011172a 100644
--- a/tests/spec/oracle/array_typedef.res.oracle
+++ b/tests/spec/oracle/array_typedef.res.oracle
@@ -71,7 +71,7 @@ struct __anonstruct_msg_1 {
 };
 typedef struct __anonstruct_msg_1 msg;
 /*@ assigns \empty; */
-void send_addr(int const * /*[4]*/ addr);
+void send_addr(int const addr[4]);
 
 void send_msg(msg const *msg)
 {
@@ -79,7 +79,7 @@ void send_msg(msg const *msg)
   return;
 }
 
-void host_address(int * /*[4]*/ ip)
+void host_address(int ip[4])
 {
   unsigned int i = sizeof(int [4]) / sizeof(int);
   *(ip + 0) = 192;
diff --git a/tests/spec/oracle/range.res.oracle b/tests/spec/oracle/range.res.oracle
index faa777bc1e4..815957073c3 100644
--- a/tests/spec/oracle/range.res.oracle
+++ b/tests/spec/oracle/range.res.oracle
@@ -13,6 +13,6 @@ int f(struct foo *x);
 
 /*@ assigns *(x + (0 .. 3));
     assigns *(x + (0 .. 3)) \from y->bli[0 .. 3]; */
-int g(char * /*[4]*/ x, struct bli *y);
+int g(char x[4], struct bli *y);
 
 
diff --git a/tests/spec/oracle/rm_qualifiers.res.oracle b/tests/spec/oracle/rm_qualifiers.res.oracle
index c1fcfb54dce..574e868cb0a 100644
--- a/tests/spec/oracle/rm_qualifiers.res.oracle
+++ b/tests/spec/oracle/rm_qualifiers.res.oracle
@@ -5,7 +5,7 @@ extern void G(void const *p);
 
 void *ptr;
 /*@ ensures ptr ≡ (void *)((int const volatile *)*(\old(ftab) + 1)); */
-void F(int const volatile (*ftab)[3], unsigned int const id)
+void F(int const volatile ftab[42][3], unsigned int const id)
 {
   G((void const *)(*(ftab + 1)));
   return;
diff --git a/tests/spec/oracle/tsets.res.oracle b/tests/spec/oracle/tsets.res.oracle
index a9a8c570ca5..3b6e704b272 100644
--- a/tests/spec/oracle/tsets.res.oracle
+++ b/tests/spec/oracle/tsets.res.oracle
@@ -37,7 +37,7 @@ int f(struct foo *x);
 
 /*@ assigns *(x + (0 .. 3));
     assigns *(x + (0 .. 3)) \from y->bli[0 .. 3]; */
-int g(char * /*[4]*/ x, struct bli *y);
+int g(char x[4], struct bli *y);
 
 int main(void)
 {
diff --git a/tests/syntax/oracle/assembly_gmp.0.res.oracle b/tests/syntax/oracle/assembly_gmp.0.res.oracle
index eb6853729c5..dcbed5fdbd3 100644
--- a/tests/syntax/oracle/assembly_gmp.0.res.oracle
+++ b/tests/syntax/oracle/assembly_gmp.0.res.oracle
@@ -14,7 +14,7 @@ void udiv_rnnd_preinv(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);
 extern int ( /* missing proto */ USItype)(long x_0);
 
 mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
-                       mp_limb_t const * /*[4]*/ bmodb)
+                       mp_limb_t const bmodb[4])
 {
   mp_limb_t __retres;
   int cnt;
diff --git a/tests/syntax/oracle/assembly_gmp.1.res.oracle b/tests/syntax/oracle/assembly_gmp.1.res.oracle
index 70ffc4d780c..fd13a956c40 100644
--- a/tests/syntax/oracle/assembly_gmp.1.res.oracle
+++ b/tests/syntax/oracle/assembly_gmp.1.res.oracle
@@ -10,7 +10,7 @@ void ADDC_LIMB(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);
 void udiv_rnnd_preinv(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);
 
 mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
-                       mp_limb_t const * /*[4]*/ bmodb)
+                       mp_limb_t const bmodb[4])
 {
   mp_limb_t __retres;
   int cnt;
diff --git a/tests/syntax/oracle/assembly_gmp.2.res.oracle b/tests/syntax/oracle/assembly_gmp.2.res.oracle
index d3e9aca3737..aef33d21f3c 100644
--- a/tests/syntax/oracle/assembly_gmp.2.res.oracle
+++ b/tests/syntax/oracle/assembly_gmp.2.res.oracle
@@ -10,7 +10,7 @@ void ADDC_LIMB(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);
 void udiv_rnnd_preinv(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);
 
 mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
-                       mp_limb_t const * /*[4]*/ bmodb)
+                       mp_limb_t const bmodb[4])
 {
   mp_limb_t __retres;
   int cnt;
diff --git a/tests/syntax/oracle/bts0519.0.res.oracle b/tests/syntax/oracle/bts0519.0.res.oracle
index 6067683d651..e99f65bdd42 100644
--- a/tests/syntax/oracle/bts0519.0.res.oracle
+++ b/tests/syntax/oracle/bts0519.0.res.oracle
@@ -1,7 +1,7 @@
 [kernel] Parsing tests/syntax/bts0519.c (with preprocessing)
 /* Generated by Frama-C */
 int t[4];
-void f(int * /*[3]*/ /* static */ a)
+void f(int a[static 3])
 {
   *(a + 2) = 3;
   return;
diff --git a/tests/syntax/oracle/dangerous_expressions.res.oracle b/tests/syntax/oracle/dangerous_expressions.res.oracle
index 668beae96e2..028e80a043e 100644
--- a/tests/syntax/oracle/dangerous_expressions.res.oracle
+++ b/tests/syntax/oracle/dangerous_expressions.res.oracle
@@ -8,7 +8,7 @@ struct __anonstruct_ss_1 {
    struct s s2 ;
 };
 struct __anonstruct_ss_1 ss;
-int f(int * /*[10]*/ t, int n, int *ptr)
+int f(int t[10], int n, int *ptr)
 {
   int __retres;
   int tmp = *(t + n);
diff --git a/tests/syntax/oracle/enum_size_array.res.oracle b/tests/syntax/oracle/enum_size_array.res.oracle
index e9d1a90b22b..e78bdab3974 100644
--- a/tests/syntax/oracle/enum_size_array.res.oracle
+++ b/tests/syntax/oracle/enum_size_array.res.oracle
@@ -5,7 +5,7 @@ enum __anonenum_T_E_1 {
     TWO = 1,
     EN_NB = 2
 };
-int f_return_last(int * /*[2]*/ tab)
+int f_return_last(int tab[2])
 {
   int __retres;
   __retres = *(tab + (EN_NB - 1));
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index b913fb80887..5d7b6e10f73 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -1001,7 +1001,7 @@ int t_main3_2[3][4][5];
     assigns (*(b + (0 .. 2)))[0 .. 3][0 .. 4]
       \from (*a)[0 .. 7], (*(b + (0 .. 2)))[0 .. 3][0 .. 4];
  */
-int main3(int (*a)[8], int (* /*[3]*/ b)[4][5]);
+int main3(int (*a)[8], int b[3][4][5]);
 
 ts t_main4[1000];
 ts u_main4[100];
-- 
GitLab