diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle index dd2862c8e5fdd14f69919031b75ba4948b247896..7923384e2abc16bd19a39ce72904917b804c210e 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 259a1cacb16867e3efdd89d5e0c0740b641955ef..994ecf230487fad2663d6d9125543bfef2d762c4 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 fc4bf6922137156c245f4e5f980663b4e20c8f66..660db18e3fa68b711fcb1904dc37b99d0519436b 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 f0925319e7706c383fc2beb1a359ab5b0c68293f..e38819902b0aa425449261ceb23c705ae1d4abff 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 798296c18a980b5a0097406083c7dc48f66302de..ba73c933112f552a9ba3d74d4a72cc6d8b678c30 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 d355aff8a40e29537ff7c18ffb93fd057512fd4b..545f2fa144a4428e2d46374c516fa7f42092a26f 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 e139ffdc57f5b105cf446018436b26a64512dff5..9455596589a8251499921bc9d809de03f2277ff9 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 8390d1842cfd8015387e9f05d813f988f2e0609b..f3cd10d4f636c230562486dffa99931989416c0b 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 8e702b9380666db861ecbfbff70c2452e01a9362..15020c1bad8499b52a7bafffa2da0cd38154c5b2 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 a6d94451ed9d58297958775a4de53c6efa8ec8e0..d502027cdad6e8c0b730ea6ed3722450ede76e21 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 51da3e81b847059d1e847ddc3d83ac4ff39b6b75..0175011172a11849177a3a60a0a339ba40a3ac34 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 faa777bc1e4760637a0dc74c0ab28cb2fa1ab2b6..815957073c38b7a0ff8eaa358fab0136b6622303 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 c1fcfb54dce01b8338946cf06f02e27845482c67..574e868cb0a451e807e172dfa524b2ad579be589 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 a9a8c570ca5c828148d41f9e4a9bae8ea2c341d7..3b6e704b2725cf21f765e51a8c474db691b31ce2 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 eb6853729c532ff192694d011b4a8e2b0a5795db..dcbed5fdbd3b7853a0150ba8d4d2331b28effe11 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 70ffc4d780c3a76abd0e4e060e91dec0c49f39e2..fd13a956c401a8705060b340d8f45e99ef4f87ac 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 d3e9aca3737cce222093576d7e70a7e44cf4d481..aef33d21f3c315f3df05dd5c7cbc794e06581a15 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 6067683d651f634b92190a87326f54d3d582f447..e99f65bdd428027981eacdc35537a7823b5837a3 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 668beae96e2173ccea281acb42342a0a13616be6..028e80a043e66a88522aba89cbdab137491720f3 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 e9d1a90b22bc8ef96390eaed45ec7280159ba73c..e78bdab39741d0abe34f3259628cbaa59315fc60 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 b913fb80887aa9d5a866a7fc270b8a95bd1ab620..5d7b6e10f73da4fc623876ff8d11b08b3625bba4 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];