Skip to content
Snippets Groups Projects
Commit 11d48df2 authored by Basile Desloges's avatar Basile Desloges Committed by Andre Maroneze
Browse files

[instantiate] Update tests for new default machdep

parent f7ae4f77
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 388 additions and 374 deletions
src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
+ 3
− 0
View file @ 11d48df2
/* run.config
STDOPT: #"-machdep x86_32"
*/
#include <stddef.h> #include <stddef.h>
void* malloc(size_t s); void* malloc(size_t s);
......
src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+ 20
− 20
View file @ 11d48df2
...@@ -300,17 +300,17 @@ int *calloc_int(size_t num, size_t size) ...@@ -300,17 +300,17 @@ int *calloc_int(size_t num, size_t size)
int main(void) int main(void)
{ {
int __retres; int __retres;
int *pi = calloc_int((unsigned int)10,sizeof(int)); int *pi = calloc_int((unsigned long)10,sizeof(int));
enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E)); enum E *pe = calloc_e_E((unsigned long)10,sizeof(enum E));
float *pf = calloc_float((unsigned int)10,sizeof(float)); float *pf = calloc_float((unsigned long)10,sizeof(float));
struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X)); struct X *px = calloc_st_X((unsigned long)10,sizeof(struct X));
char *pc = calloc_char((unsigned int)10,sizeof(char)); char *pc = calloc_char((unsigned long)10,sizeof(char));
int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10])); int (*pa)[10] = calloc_arr10_int((unsigned long)10,sizeof(int [10]));
struct Flex *f = struct Flex *f =
calloc_st_Flex((unsigned int)1, calloc_st_Flex((unsigned long)1,
sizeof(struct Flex) + (unsigned int)3 * sizeof(int)); sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
void *v = calloc((unsigned int)10,sizeof(char)); void *v = calloc((unsigned long)10,sizeof(char));
struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10); struct incomplete *inc = calloc((unsigned long)10,(unsigned long)10);
__retres = 0; __retres = 0;
return __retres; return __retres;
} }
...@@ -619,17 +619,17 @@ int *calloc_int(size_t num, size_t size) ...@@ -619,17 +619,17 @@ int *calloc_int(size_t num, size_t size)
int main(void) int main(void)
{ {
int __retres; int __retres;
int *pi = calloc_int((unsigned int)10,sizeof(int)); int *pi = calloc_int((unsigned long)10,sizeof(int));
enum E *pe = calloc_e_E((unsigned int)10,sizeof(enum E)); enum E *pe = calloc_e_E((unsigned long)10,sizeof(enum E));
float *pf = calloc_float((unsigned int)10,sizeof(float)); float *pf = calloc_float((unsigned long)10,sizeof(float));
struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X)); struct X *px = calloc_st_X((unsigned long)10,sizeof(struct X));
char *pc = calloc_char((unsigned int)10,sizeof(char)); char *pc = calloc_char((unsigned long)10,sizeof(char));
int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10])); int (*pa)[10] = calloc_arr10_int((unsigned long)10,sizeof(int [10]));
struct Flex *f = struct Flex *f =
calloc_st_Flex((unsigned int)1, calloc_st_Flex((unsigned long)1,
sizeof(struct Flex) + (unsigned int)3 * sizeof(int)); sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
void *v = calloc((unsigned int)10,sizeof(char)); void *v = calloc((unsigned long)10,sizeof(char));
struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10); struct incomplete *inc = calloc((unsigned long)10,(unsigned long)10);
__retres = 0; __retres = 0;
return __retres; return __retres;
} }
......
src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
+ 16
− 16
View file @ 11d48df2
...@@ -204,15 +204,15 @@ int *malloc_int(size_t size) ...@@ -204,15 +204,15 @@ int *malloc_int(size_t size)
int main(void) int main(void)
{ {
int __retres; int __retres;
int *pi = malloc_int(sizeof(int) * (unsigned int)10); int *pi = malloc_int(sizeof(int) * (unsigned long)10);
float *pf = malloc_float(sizeof(float) * (unsigned int)10); float *pf = malloc_float(sizeof(float) * (unsigned long)10);
struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10); struct X *px = malloc_st_X(sizeof(struct X) * (unsigned long)10);
char *pc = malloc_char((unsigned int)10); char *pc = malloc_char((unsigned long)10);
int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10); int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned long)10);
struct Flex *f = struct Flex *f =
malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int)); malloc_st_Flex(sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
void *v = malloc(sizeof(char) * (unsigned int)10); void *v = malloc(sizeof(char) * (unsigned long)10);
struct incomplete *inc = malloc((unsigned int)10); struct incomplete *inc = malloc((unsigned long)10);
__retres = 0; __retres = 0;
return __retres; return __retres;
} }
...@@ -420,15 +420,15 @@ int *malloc_int(size_t size) ...@@ -420,15 +420,15 @@ int *malloc_int(size_t size)
int main(void) int main(void)
{ {
int __retres; int __retres;
int *pi = malloc_int(sizeof(int) * (unsigned int)10); int *pi = malloc_int(sizeof(int) * (unsigned long)10);
float *pf = malloc_float(sizeof(float) * (unsigned int)10); float *pf = malloc_float(sizeof(float) * (unsigned long)10);
struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10); struct X *px = malloc_st_X(sizeof(struct X) * (unsigned long)10);
char *pc = malloc_char((unsigned int)10); char *pc = malloc_char((unsigned long)10);
int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10); int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned long)10);
struct Flex *f = struct Flex *f =
malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int)); malloc_st_Flex(sizeof(struct Flex) + (unsigned long)3 * sizeof(int));
void *v = malloc(sizeof(char) * (unsigned int)10); void *v = malloc(sizeof(char) * (unsigned long)10);
struct incomplete *inc = malloc((unsigned int)10); struct incomplete *inc = malloc((unsigned long)10);
__retres = 0; __retres = 0;
return __retres; return __retres;
} }
......
src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+ 34
− 34
View file @ 11d48df2
...@@ -48,14 +48,14 @@ int memcmp_int(int const *s1, int const *s2, size_t len) ...@@ -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 integer(int * /*[10]*/ s1, int * /*[10]*/ s2)
{ {
int tmp; int tmp;
tmp = memcmp_int(s1,s2,(unsigned int)10 * sizeof(int)); tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(int));
return tmp; return tmp;
} }
int with_named(named * /*[10]*/ s1, named * /*[10]*/ s2) int with_named(named * /*[10]*/ s1, named * /*[10]*/ s2)
{ {
int tmp; int tmp;
tmp = memcmp_int(s1,s2,(unsigned int)10 * sizeof(named)); tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(named));
return tmp; return tmp;
} }
...@@ -86,26 +86,26 @@ int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len) ...@@ -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 structure(struct X * /*[10]*/ s1, struct X * /*[10]*/ s2)
{ {
int tmp; 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; return tmp;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires requires
valid_read_s1: 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 requires
valid_read_s2: 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 ensures
equals: equals:
\let __fc_len = len / 4; \let __fc_len = len / 8;
\result ≡ 0 ⇔ \result ≡ 0 ⇔
(∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0)); (∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
assigns \result; assigns \result;
assigns \result assigns \result
\from (indirect: *(s1 + (0 .. len / 4 - 1))), \from (indirect: *(s1 + (0 .. len / 8 - 1))),
(indirect: *(s2 + (0 .. len / 4 - 1))); (indirect: *(s2 + (0 .. len / 8 - 1)));
*/ */
int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len) 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) ...@@ -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 pointers(int ** /*[10]*/ s1, int ** /*[10]*/ s2)
{ {
int tmp; 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; return tmp;
} }
...@@ -151,32 +151,32 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len) ...@@ -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 nested(int (*s1)[10], int (*s2)[10], int n)
{ {
int tmp; 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; return tmp;
} }
int with_void(void *s1, void *s2, int n) int with_void(void *s1, void *s2, int n)
{ {
int tmp; 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; return tmp;
} }
int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n) int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
{ {
int tmp; 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; return tmp;
} }
void with_null_or_int(int * /*[10]*/ p) void with_null_or_int(int * /*[10]*/ p)
{ {
memcmp((void const *)0,(void const *)p,(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 int)10 * sizeof(int)); memcmp((void const *)p,(void const *)0,(unsigned long)10 * sizeof(int));
memcmp((void const *)((int const *)42),(void const *)p, 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), memcmp((void const *)p,(void const *)((int const *)42),
(unsigned int)10 * sizeof(int)); (unsigned long)10 * sizeof(int));
return; return;
} }
...@@ -221,7 +221,7 @@ int integer(int *s1, int *s2) ...@@ -221,7 +221,7 @@ int integer(int *s1, int *s2)
{ {
int tmp; int tmp;
tmp = memcmp_int((int const *)s1,(int const *)s2, tmp = memcmp_int((int const *)s1,(int const *)s2,
(unsigned int)10 * sizeof(int)); (unsigned long)10 * sizeof(int));
return tmp; return tmp;
} }
...@@ -229,7 +229,7 @@ int with_named(named *s1, named *s2) ...@@ -229,7 +229,7 @@ int with_named(named *s1, named *s2)
{ {
int tmp; int tmp;
tmp = memcmp_int((int const *)s1,(int const *)s2, tmp = memcmp_int((int const *)s1,(int const *)s2,
(unsigned int)10 * sizeof(named)); (unsigned long)10 * sizeof(named));
return tmp; return tmp;
} }
...@@ -262,27 +262,27 @@ int structure(struct X *s1, struct X *s2) ...@@ -262,27 +262,27 @@ int structure(struct X *s1, struct X *s2)
{ {
int tmp; int tmp;
tmp = memcmp_st_X((struct X const *)s1,(struct X const *)s2, 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; return tmp;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires requires
valid_read_s1: 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 requires
valid_read_s2: 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 ensures
equals: equals:
\let __fc_len = \old(len) / 4; \let __fc_len = \old(len) / 8;
\result ≡ 0 ⇔ \result ≡ 0 ⇔
(∀ ℤ j0; (∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0)); 0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0));
assigns \result; assigns \result;
assigns \result assigns \result
\from (indirect: *(s1 + (0 .. len / 4 - 1))), \from (indirect: *(s1 + (0 .. len / 8 - 1))),
(indirect: *(s2 + (0 .. len / 4 - 1))); (indirect: *(s2 + (0 .. len / 8 - 1)));
*/ */
int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len) int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
{ {
...@@ -295,7 +295,7 @@ int pointers(int **s1, int **s2) ...@@ -295,7 +295,7 @@ int pointers(int **s1, int **s2)
{ {
int tmp; int tmp;
tmp = memcmp_ptr_int((int * const *)s1,(int * const *)s2, tmp = memcmp_ptr_int((int * const *)s1,(int * const *)s2,
(unsigned int)10 * sizeof(int *)); (unsigned long)10 * sizeof(int *));
return tmp; return tmp;
} }
...@@ -331,32 +331,32 @@ int nested(int (*s1)[10], int (*s2)[10], int n) ...@@ -331,32 +331,32 @@ int nested(int (*s1)[10], int (*s2)[10], int n)
{ {
int tmp; int tmp;
tmp = memcmp_arr10_int((int const (*)[10])s1,(int const (*)[10])s2, 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; return tmp;
} }
int with_void(void *s1, void *s2, int n) int with_void(void *s1, void *s2, int n)
{ {
int tmp; 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; return tmp;
} }
int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n) int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
{ {
int tmp; 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; return tmp;
} }
void with_null_or_int(int *p) void with_null_or_int(int *p)
{ {
memcmp((void const *)0,(void const *)p,(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 int)10 * sizeof(int)); memcmp((void const *)p,(void const *)0,(unsigned long)10 * sizeof(int));
memcmp((void const *)((int const *)42),(void const *)p, 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), memcmp((void const *)p,(void const *)((int const *)42),
(unsigned int)10 * sizeof(int)); (unsigned long)10 * sizeof(int));
return; return;
} }
......
src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+ 50
− 50
View file @ 11d48df2
...@@ -53,15 +53,15 @@ int *memcpy_int(int *dest, int const *src, size_t len) ...@@ -53,15 +53,15 @@ int *memcpy_int(int *dest, int const *src, size_t len)
void integer(int * /*[10]*/ src, int * /*[10]*/ dest) void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
{ {
int *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(int)); int *res = memcpy_int(dest,src,(unsigned long)10 * sizeof(int));
memcpy_int(src,res,(unsigned int)10 * sizeof(int)); memcpy_int(src,res,(unsigned long)10 * sizeof(int));
return; return;
} }
void with_named(named * /*[10]*/ src, named * /*[10]*/ dest) void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
{ {
named *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(named)); named *res = memcpy_int(dest,src,(unsigned long)10 * sizeof(named));
memcpy_int(src,res,(unsigned int)10 * sizeof(named)); memcpy_int(src,res,(unsigned long)10 * sizeof(named));
return; return;
} }
...@@ -93,28 +93,28 @@ struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len) ...@@ -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) void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
{ {
struct X *res = memcpy_st_X(dest,src,(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 int)10 * sizeof(struct X)); memcpy_st_X(src,res,(unsigned long)10 * sizeof(struct X));
return; return;
} }
/*@ requires /*@ requires
separation: separation:
\let __fc_len = len / 4; \let __fc_len = len / 8;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1)); \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
requires aligned_end: len % 4 ≡ 0; requires aligned_end: len % 8 ≡ 0;
requires 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 requires
valid_read_src: 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 ensures
copied: copied:
\let __fc_len = len / 4; \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0); ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
ensures result: \result ≡ dest; ensures result: \result ≡ dest;
assigns *(dest + (0 .. len / 4 - 1)), \result; assigns *(dest + (0 .. len / 8 - 1)), \result;
assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1)); assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest; assigns \result \from dest;
*/ */
int **memcpy_ptr_int(int **dest, int * const *src, size_t len) 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) ...@@ -126,8 +126,8 @@ int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest) void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
{ {
int **res = memcpy_ptr_int(dest,src,(unsigned int)10 * sizeof(int *)); int **res = memcpy_ptr_int(dest,src,(unsigned long)10 * sizeof(int *));
memcpy_ptr_int(src,res,(unsigned int)10 * sizeof(int *)); memcpy_ptr_int(src,res,(unsigned long)10 * sizeof(int *));
return; return;
} }
...@@ -165,32 +165,32 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10] ...@@ -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) void nested(int (*src)[10], int (*dest)[10], int n)
{ {
int (*res)[10] = int (*res)[10] =
memcpy_arr10_int(dest,src,(unsigned int)n * sizeof(int [10])); memcpy_arr10_int(dest,src,(unsigned long)n * sizeof(int [10]));
memcpy_arr10_int(src,res,(unsigned int)n * sizeof(int [10])); memcpy_arr10_int(src,res,(unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *src, void *dest, int n) void with_void(void *src, void *dest, int n)
{ {
void *res = memcpy(dest,(void const *)src,(unsigned int)n); void *res = memcpy(dest,(void const *)src,(unsigned long)n);
memcpy(src,(void const *)res,(unsigned int)n); memcpy(src,(void const *)res,(unsigned long)n);
return; return;
} }
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n) void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{ {
struct incomplete *res = struct incomplete *res =
memcpy((void *)dest,(void const *)src,(unsigned int)n); memcpy((void *)dest,(void const *)src,(unsigned long)n);
memcpy((void *)src,(void const *)res,(unsigned int)n); memcpy((void *)src,(void const *)res,(unsigned long)n);
return; return;
} }
void with_null_or_int(int * /*[10]*/ p) void with_null_or_int(int * /*[10]*/ p)
{ {
memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int)); memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int)); memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int)); memcpy((void *)((int *)42),(void const *)p,(unsigned long)10 * sizeof(int));
memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int)); memcpy((void *)p,(void const *)((int *)42),(unsigned long)10 * sizeof(int));
return; return;
} }
...@@ -236,16 +236,16 @@ int *memcpy_int(int *dest, int const *src, size_t len) ...@@ -236,16 +236,16 @@ int *memcpy_int(int *dest, int const *src, size_t len)
void integer(int *src, int *dest) void integer(int *src, int *dest)
{ {
int *res = int *res =
memcpy_int(dest,(int const *)src,(unsigned int)10 * sizeof(int)); memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(int));
memcpy_int(src,(int const *)res,(unsigned int)10 * sizeof(int)); memcpy_int(src,(int const *)res,(unsigned long)10 * sizeof(int));
return; return;
} }
void with_named(named *src, named *dest) void with_named(named *src, named *dest)
{ {
named *res = named *res =
memcpy_int(dest,(int const *)src,(unsigned int)10 * sizeof(named)); memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(named));
memcpy_int(src,(int const *)res,(unsigned int)10 * sizeof(named)); memcpy_int(src,(int const *)res,(unsigned long)10 * sizeof(named));
return; return;
} }
...@@ -280,29 +280,29 @@ void structure(struct X *src, struct X *dest) ...@@ -280,29 +280,29 @@ void structure(struct X *src, struct X *dest)
{ {
struct X *res = struct X *res =
memcpy_st_X(dest,(struct X const *)src, memcpy_st_X(dest,(struct X const *)src,
(unsigned int)10 * sizeof(struct X)); (unsigned long)10 * sizeof(struct X));
memcpy_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X)); memcpy_st_X(src,(struct X const *)res,(unsigned long)10 * sizeof(struct X));
return; return;
} }
/*@ requires /*@ requires
separation: separation:
\let __fc_len = len / 4; \let __fc_len = len / 8;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1)); \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
requires aligned_end: len % 4 ≡ 0; requires aligned_end: len % 8 ≡ 0;
requires 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 requires
valid_read_src: 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 ensures
copied: copied:
\let __fc_len = \old(len) / 4; \let __fc_len = \old(len) / 8;
∀ ℤ j0; ∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0); 0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
ensures result: \result ≡ \old(dest); ensures result: \result ≡ \old(dest);
assigns *(dest + (0 .. len / 4 - 1)), \result; assigns *(dest + (0 .. len / 8 - 1)), \result;
assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1)); assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest; assigns \result \from dest;
*/ */
int **memcpy_ptr_int(int **dest, int * const *src, size_t len) 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) ...@@ -315,8 +315,8 @@ int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
void pointers(int **src, int **dest) void pointers(int **src, int **dest)
{ {
int **res = int **res =
memcpy_ptr_int(dest,(int * const *)src,(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 int)10 * sizeof(int *)); memcpy_ptr_int(src,(int * const *)res,(unsigned long)10 * sizeof(int *));
return; return;
} }
...@@ -356,33 +356,33 @@ void nested(int (*src)[10], int (*dest)[10], int n) ...@@ -356,33 +356,33 @@ void nested(int (*src)[10], int (*dest)[10], int n)
{ {
int (*res)[10] = int (*res)[10] =
memcpy_arr10_int(dest,(int const (*)[10])src, 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, memcpy_arr10_int(src,(int const (*)[10])res,
(unsigned int)n * sizeof(int [10])); (unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *src, void *dest, int n) void with_void(void *src, void *dest, int n)
{ {
void *res = memcpy(dest,(void const *)src,(unsigned int)n); void *res = memcpy(dest,(void const *)src,(unsigned long)n);
memcpy(src,(void const *)res,(unsigned int)n); memcpy(src,(void const *)res,(unsigned long)n);
return; return;
} }
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n) void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{ {
struct incomplete *res = struct incomplete *res =
memcpy((void *)dest,(void const *)src,(unsigned int)n); memcpy((void *)dest,(void const *)src,(unsigned long)n);
memcpy((void *)src,(void const *)res,(unsigned int)n); memcpy((void *)src,(void const *)res,(unsigned long)n);
return; return;
} }
void with_null_or_int(int *p) void with_null_or_int(int *p)
{ {
memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int)); memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int)); memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int)); memcpy((void *)((int *)42),(void const *)p,(unsigned long)10 * sizeof(int));
memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int)); memcpy((void *)p,(void const *)((int *)42),(unsigned long)10 * sizeof(int));
return; return;
} }
......
src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+ 55
− 48
View file @ 11d48df2
...@@ -49,15 +49,15 @@ int *memmove_int(int *dest, int const *src, size_t len) ...@@ -49,15 +49,15 @@ int *memmove_int(int *dest, int const *src, size_t len)
void integer(int * /*[10]*/ src, int * /*[10]*/ dest) void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
{ {
int *res = memmove_int(dest,src,(unsigned int)10 * sizeof(int)); int *res = memmove_int(dest,src,(unsigned long)10 * sizeof(int));
memmove_int(src,res,(unsigned int)10 * sizeof(int)); memmove_int(src,res,(unsigned long)10 * sizeof(int));
return; return;
} }
void with_named(named * /*[10]*/ src, named * /*[10]*/ dest) void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
{ {
named *res = memmove_int(dest,src,(unsigned int)10 * sizeof(named)); named *res = memmove_int(dest,src,(unsigned long)10 * sizeof(named));
memmove_int(src,res,(unsigned int)10 * sizeof(named)); memmove_int(src,res,(unsigned long)10 * sizeof(named));
return; return;
} }
...@@ -85,24 +85,25 @@ struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len) ...@@ -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) void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
{ {
struct X *res = memmove_st_X(dest,src,(unsigned int)10 * sizeof(struct X)); struct X *res =
memmove_st_X(src,res,(unsigned int)10 * sizeof(struct X)); memmove_st_X(dest,src,(unsigned long)10 * sizeof(struct X));
memmove_st_X(src,res,(unsigned long)10 * sizeof(struct X));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 requires
valid_read_src: 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 ensures
moved: moved:
\let __fc_len = len / 4; \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0); ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
ensures result: \result ≡ dest; ensures result: \result ≡ dest;
assigns *(dest + (0 .. len / 4 - 1)), \result; assigns *(dest + (0 .. len / 8 - 1)), \result;
assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1)); assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest; assigns \result \from dest;
*/ */
int **memmove_ptr_int(int **dest, int * const *src, size_t len) 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) ...@@ -114,8 +115,8 @@ int **memmove_ptr_int(int **dest, int * const *src, size_t len)
void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest) void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
{ {
int **res = memmove_ptr_int(dest,src,(unsigned int)10 * sizeof(int *)); int **res = memmove_ptr_int(dest,src,(unsigned long)10 * sizeof(int *));
memmove_ptr_int(src,res,(unsigned int)10 * sizeof(int *)); memmove_ptr_int(src,res,(unsigned long)10 * sizeof(int *));
return; return;
} }
...@@ -149,32 +150,34 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10] ...@@ -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) void nested(int (*src)[10], int (*dest)[10], int n)
{ {
int (*res)[10] = int (*res)[10] =
memmove_arr10_int(dest,src,(unsigned int)n * sizeof(int [10])); memmove_arr10_int(dest,src,(unsigned long)n * sizeof(int [10]));
memmove_arr10_int(src,res,(unsigned int)n * sizeof(int [10])); memmove_arr10_int(src,res,(unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *src, void *dest, int n) void with_void(void *src, void *dest, int n)
{ {
void *res = memmove(dest,(void const *)src,(unsigned int)n); void *res = memmove(dest,(void const *)src,(unsigned long)n);
memmove(src,(void const *)res,(unsigned int)n); memmove(src,(void const *)res,(unsigned long)n);
return; return;
} }
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n) void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{ {
struct incomplete *res = struct incomplete *res =
memmove((void *)dest,(void const *)src,(unsigned int)n); memmove((void *)dest,(void const *)src,(unsigned long)n);
memmove((void *)src,(void const *)res,(unsigned int)n); memmove((void *)src,(void const *)res,(unsigned long)n);
return; return;
} }
void with_null_or_int(int * /*[10]*/ p) void with_null_or_int(int * /*[10]*/ p)
{ {
memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int)); memmove((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int)); memmove((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int)); memmove((void *)((int *)42),(void const *)p,
memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int)); (unsigned long)10 * sizeof(int));
memmove((void *)p,(void const *)((int *)42),
(unsigned long)10 * sizeof(int));
return; return;
} }
...@@ -216,16 +219,16 @@ int *memmove_int(int *dest, int const *src, size_t len) ...@@ -216,16 +219,16 @@ int *memmove_int(int *dest, int const *src, size_t len)
void integer(int *src, int *dest) void integer(int *src, int *dest)
{ {
int *res = int *res =
memmove_int(dest,(int const *)src,(unsigned int)10 * sizeof(int)); memmove_int(dest,(int const *)src,(unsigned long)10 * sizeof(int));
memmove_int(src,(int const *)res,(unsigned int)10 * sizeof(int)); memmove_int(src,(int const *)res,(unsigned long)10 * sizeof(int));
return; return;
} }
void with_named(named *src, named *dest) void with_named(named *src, named *dest)
{ {
named *res = named *res =
memmove_int(dest,(int const *)src,(unsigned int)10 * sizeof(named)); memmove_int(dest,(int const *)src,(unsigned long)10 * sizeof(named));
memmove_int(src,(int const *)res,(unsigned int)10 * sizeof(named)); memmove_int(src,(int const *)res,(unsigned long)10 * sizeof(named));
return; return;
} }
...@@ -256,25 +259,26 @@ void structure(struct X *src, struct X *dest) ...@@ -256,25 +259,26 @@ void structure(struct X *src, struct X *dest)
{ {
struct X *res = struct X *res =
memmove_st_X(dest,(struct X const *)src, memmove_st_X(dest,(struct X const *)src,
(unsigned int)10 * sizeof(struct X)); (unsigned long)10 * sizeof(struct X));
memmove_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X)); memmove_st_X(src,(struct X const *)res,
(unsigned long)10 * sizeof(struct X));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 requires
valid_read_src: 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 ensures
moved: moved:
\let __fc_len = \old(len) / 4; \let __fc_len = \old(len) / 8;
∀ ℤ j0; ∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0); 0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
ensures result: \result ≡ \old(dest); ensures result: \result ≡ \old(dest);
assigns *(dest + (0 .. len / 4 - 1)), \result; assigns *(dest + (0 .. len / 8 - 1)), \result;
assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1)); assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
assigns \result \from dest; assigns \result \from dest;
*/ */
int **memmove_ptr_int(int **dest, int * const *src, size_t len) 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) ...@@ -287,8 +291,9 @@ int **memmove_ptr_int(int **dest, int * const *src, size_t len)
void pointers(int **src, int **dest) void pointers(int **src, int **dest)
{ {
int **res = int **res =
memmove_ptr_int(dest,(int * const *)src,(unsigned int)10 * sizeof(int *)); memmove_ptr_int(dest,(int * const *)src,
memmove_ptr_int(src,(int * const *)res,(unsigned int)10 * sizeof(int *)); (unsigned long)10 * sizeof(int *));
memmove_ptr_int(src,(int * const *)res,(unsigned long)10 * sizeof(int *));
return; return;
} }
...@@ -324,33 +329,35 @@ void nested(int (*src)[10], int (*dest)[10], int n) ...@@ -324,33 +329,35 @@ void nested(int (*src)[10], int (*dest)[10], int n)
{ {
int (*res)[10] = int (*res)[10] =
memmove_arr10_int(dest,(int const (*)[10])src, 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, memmove_arr10_int(src,(int const (*)[10])res,
(unsigned int)n * sizeof(int [10])); (unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *src, void *dest, int n) void with_void(void *src, void *dest, int n)
{ {
void *res = memmove(dest,(void const *)src,(unsigned int)n); void *res = memmove(dest,(void const *)src,(unsigned long)n);
memmove(src,(void const *)res,(unsigned int)n); memmove(src,(void const *)res,(unsigned long)n);
return; return;
} }
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n) void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{ {
struct incomplete *res = struct incomplete *res =
memmove((void *)dest,(void const *)src,(unsigned int)n); memmove((void *)dest,(void const *)src,(unsigned long)n);
memmove((void *)src,(void const *)res,(unsigned int)n); memmove((void *)src,(void const *)res,(unsigned long)n);
return; return;
} }
void with_null_or_int(int *p) void with_null_or_int(int *p)
{ {
memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int)); memmove((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int)); memmove((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int)); memmove((void *)((int *)42),(void const *)p,
memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int)); (unsigned long)10 * sizeof(int));
memmove((void *)p,(void const *)((int *)42),
(unsigned long)10 * sizeof(int));
return; return;
} }
......
src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+ 58
− 58
View file @ 11d48df2
...@@ -39,8 +39,8 @@ char *memset_char(char *ptr, char value, size_t len) ...@@ -39,8 +39,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char * /*[10]*/ dest) void chars(char * /*[10]*/ dest)
{ {
char *res = memset_char(dest,(char)0,(unsigned int)10); char *res = memset_char(dest,(char)0,(unsigned long)10);
memset_char(res,(char)0,(unsigned int)10); memset_char(res,(char)0,(unsigned long)10);
return; return;
} }
...@@ -63,8 +63,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value, ...@@ -63,8 +63,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(unsigned char * /*[10]*/ dest) void uchars(unsigned char * /*[10]*/ dest)
{ {
unsigned char *res = memset_uchar(dest,(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 int)10); memset_uchar(res,(unsigned char)0,(unsigned long)10);
return; return;
} }
...@@ -91,8 +91,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10] ...@@ -91,8 +91,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (* /*[10]*/ dest)[10]) void nested_chars(char (* /*[10]*/ dest)[10])
{ {
char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned int)100); char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned long)100);
memset_arr10_char(res,(char)0,(unsigned int)100); memset_arr10_char(res,(char)0,(unsigned long)100);
return; return;
} }
...@@ -117,8 +117,8 @@ int *memset_int_0(int *ptr, size_t len) ...@@ -117,8 +117,8 @@ int *memset_int_0(int *ptr, size_t len)
void integer(int * /*[10]*/ dest) void integer(int * /*[10]*/ dest)
{ {
int *res = memset_int_0(dest,(unsigned int)10 * sizeof(int)); int *res = memset_int_0(dest,(unsigned long)10 * sizeof(int));
memset_int_0(res,(unsigned int)10 * sizeof(int)); memset_int_0(res,(unsigned long)10 * sizeof(int));
return; return;
} }
...@@ -143,8 +143,8 @@ enum E *memset_e_E_0(enum E *ptr, size_t len) ...@@ -143,8 +143,8 @@ enum E *memset_e_E_0(enum E *ptr, size_t len)
void with_enum(enum E * /*[10]*/ dest) void with_enum(enum E * /*[10]*/ dest)
{ {
enum E *res = memset_e_E_0(dest,(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 int)10 * sizeof(enum E)); memset_e_E_0(res,(unsigned long)10 * sizeof(enum E));
return; return;
} }
...@@ -169,15 +169,15 @@ float *memset_float_0(float *ptr, size_t len) ...@@ -169,15 +169,15 @@ float *memset_float_0(float *ptr, size_t len)
void floats(float * /*[10]*/ dest) void floats(float * /*[10]*/ dest)
{ {
float *res = memset_float_0(dest,(unsigned int)10 * sizeof(float)); float *res = memset_float_0(dest,(unsigned long)10 * sizeof(float));
memset_float_0(res,(unsigned int)10 * sizeof(float)); memset_float_0(res,(unsigned long)10 * sizeof(float));
return; return;
} }
void with_named(named * /*[10]*/ dest) void with_named(named * /*[10]*/ dest)
{ {
named *res = memset_int_0(dest,(unsigned int)10 * sizeof(named)); named *res = memset_int_0(dest,(unsigned long)10 * sizeof(named));
memset_int_0(res,(unsigned int)10 * sizeof(named)); memset_int_0(res,(unsigned long)10 * sizeof(named));
return; return;
} }
...@@ -203,21 +203,21 @@ struct X *memset_st_X_0(struct X *ptr, size_t len) ...@@ -203,21 +203,21 @@ struct X *memset_st_X_0(struct X *ptr, size_t len)
void structure(struct X * /*[10]*/ dest) void structure(struct X * /*[10]*/ dest)
{ {
struct X *res = memset_st_X_0(dest,(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 int)10 * sizeof(struct X)); memset_st_X_0(res,(unsigned long)10 * sizeof(struct X));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 ensures
set_content: set_content:
\let __fc_len = len / 4; \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ \null; ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ \null;
ensures result: \result ≡ ptr; ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 4 - 1)), \result; assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr; assigns \result \from ptr;
*/ */
int **memset_ptr_int_0(int **ptr, size_t len) int **memset_ptr_int_0(int **ptr, size_t len)
...@@ -229,8 +229,8 @@ 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) void pointers(int ** /*[10]*/ dest)
{ {
int **res = memset_ptr_int_0(dest,(unsigned int)10 * sizeof(int *)); int **res = memset_ptr_int_0(dest,(unsigned long)10 * sizeof(int *));
memset_ptr_int_0(res,(unsigned int)10 * sizeof(int *)); memset_ptr_int_0(res,(unsigned long)10 * sizeof(int *));
return; return;
} }
...@@ -258,22 +258,22 @@ int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10] ...@@ -258,22 +258,22 @@ int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10]
void nested(int (*dest)[10], int n) void nested(int (*dest)[10], int n)
{ {
int (*res)[10] = int (*res)[10] =
memset_arr10_int_0(dest,(unsigned int)n * sizeof(int [10])); memset_arr10_int_0(dest,(unsigned long)n * sizeof(int [10]));
memset_arr10_int_0(res,(unsigned int)n * sizeof(int [10])); memset_arr10_int_0(res,(unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *dest) void with_void(void *dest)
{ {
void *res = memset(dest,0,(unsigned int)10); void *res = memset(dest,0,(unsigned long)10);
memset(res,0,(unsigned int)10); memset(res,0,(unsigned long)10);
return; return;
} }
void with_null_or_int(void) void with_null_or_int(void)
{ {
memset((void *)0,0,(unsigned int)10); memset((void *)0,0,(unsigned long)10);
memset((void *)((int *)42),0,(unsigned int)10); memset((void *)((int *)42),0,(unsigned long)10);
return; return;
} }
...@@ -313,8 +313,8 @@ char *memset_char(char *ptr, char value, size_t len) ...@@ -313,8 +313,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char *dest) void chars(char *dest)
{ {
char *res = memset_char(dest,(char)0,(unsigned int)10); char *res = memset_char(dest,(char)0,(unsigned long)10);
memset_char(res,(char)0,(unsigned int)10); memset_char(res,(char)0,(unsigned long)10);
return; return;
} }
...@@ -339,8 +339,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value, ...@@ -339,8 +339,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(unsigned char *dest) void uchars(unsigned char *dest)
{ {
unsigned char *res = memset_uchar(dest,(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 int)10); memset_uchar(res,(unsigned char)0,(unsigned long)10);
return; return;
} }
...@@ -368,8 +368,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10] ...@@ -368,8 +368,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (*dest)[10]) void nested_chars(char (*dest)[10])
{ {
char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned int)100); char (*res)[10] = memset_arr10_char(dest,(char)0,(unsigned long)100);
memset_arr10_char(res,(char)0,(unsigned int)100); memset_arr10_char(res,(char)0,(unsigned long)100);
return; return;
} }
...@@ -394,8 +394,8 @@ int *memset_int_0(int *ptr, size_t len) ...@@ -394,8 +394,8 @@ int *memset_int_0(int *ptr, size_t len)
void integer(int *dest) void integer(int *dest)
{ {
int *res = memset_int_0(dest,(unsigned int)10 * sizeof(int)); int *res = memset_int_0(dest,(unsigned long)10 * sizeof(int));
memset_int_0(res,(unsigned int)10 * sizeof(int)); memset_int_0(res,(unsigned long)10 * sizeof(int));
return; return;
} }
...@@ -420,8 +420,8 @@ enum E *memset_e_E_0(enum E *ptr, size_t len) ...@@ -420,8 +420,8 @@ enum E *memset_e_E_0(enum E *ptr, size_t len)
void with_enum(enum E *dest) void with_enum(enum E *dest)
{ {
enum E *res = memset_e_E_0(dest,(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 int)10 * sizeof(enum E)); memset_e_E_0(res,(unsigned long)10 * sizeof(enum E));
return; return;
} }
...@@ -446,15 +446,15 @@ float *memset_float_0(float *ptr, size_t len) ...@@ -446,15 +446,15 @@ float *memset_float_0(float *ptr, size_t len)
void floats(float *dest) void floats(float *dest)
{ {
float *res = memset_float_0(dest,(unsigned int)10 * sizeof(float)); float *res = memset_float_0(dest,(unsigned long)10 * sizeof(float));
memset_float_0(res,(unsigned int)10 * sizeof(float)); memset_float_0(res,(unsigned long)10 * sizeof(float));
return; return;
} }
void with_named(named *dest) void with_named(named *dest)
{ {
named *res = memset_int_0(dest,(unsigned int)10 * sizeof(named)); named *res = memset_int_0(dest,(unsigned long)10 * sizeof(named));
memset_int_0(res,(unsigned int)10 * sizeof(named)); memset_int_0(res,(unsigned long)10 * sizeof(named));
return; return;
} }
...@@ -481,21 +481,21 @@ struct X *memset_st_X_0(struct X *ptr, size_t len) ...@@ -481,21 +481,21 @@ struct X *memset_st_X_0(struct X *ptr, size_t len)
void structure(struct X *dest) void structure(struct X *dest)
{ {
struct X *res = memset_st_X_0(dest,(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 int)10 * sizeof(struct X)); memset_st_X_0(res,(unsigned long)10 * sizeof(struct X));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 ensures
set_content: set_content:
\let __fc_len = \old(len) / 4; \let __fc_len = \old(len) / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ \null; ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ \null;
ensures result: \result ≡ \old(ptr); ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 4 - 1)), \result; assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr; assigns \result \from ptr;
*/ */
int **memset_ptr_int_0(int **ptr, size_t len) int **memset_ptr_int_0(int **ptr, size_t len)
...@@ -507,8 +507,8 @@ 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) void pointers(int **dest)
{ {
int **res = memset_ptr_int_0(dest,(unsigned int)10 * sizeof(int *)); int **res = memset_ptr_int_0(dest,(unsigned long)10 * sizeof(int *));
memset_ptr_int_0(res,(unsigned int)10 * sizeof(int *)); memset_ptr_int_0(res,(unsigned long)10 * sizeof(int *));
return; return;
} }
...@@ -536,22 +536,22 @@ int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10] ...@@ -536,22 +536,22 @@ int (*memset_arr10_int_0(int (*ptr)[10], size_t len))[10]
void nested(int (*dest)[10], int n) void nested(int (*dest)[10], int n)
{ {
int (*res)[10] = int (*res)[10] =
memset_arr10_int_0(dest,(unsigned int)n * sizeof(int [10])); memset_arr10_int_0(dest,(unsigned long)n * sizeof(int [10]));
memset_arr10_int_0(res,(unsigned int)n * sizeof(int [10])); memset_arr10_int_0(res,(unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *dest) void with_void(void *dest)
{ {
void *res = memset(dest,0,(unsigned int)10); void *res = memset(dest,0,(unsigned long)10);
memset(res,0,(unsigned int)10); memset(res,0,(unsigned long)10);
return; return;
} }
void with_null_or_int(void) void with_null_or_int(void)
{ {
memset((void *)0,0,(unsigned int)10); memset((void *)0,0,(unsigned long)10);
memset((void *)((int *)42),0,(unsigned int)10); memset((void *)((int *)42),0,(unsigned long)10);
return; return;
} }
......
src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+ 102
− 100
View file @ 11d48df2
...@@ -39,8 +39,8 @@ char *memset_char(char *ptr, char value, size_t len) ...@@ -39,8 +39,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char * /*[10]*/ dest) void chars(char * /*[10]*/ dest)
{ {
char *res = memset_char(dest,(char)0xFF,(unsigned int)10); char *res = memset_char(dest,(char)0xFF,(unsigned long)10);
memset_char(res,(char)0xFF,(unsigned int)10); memset_char(res,(char)0xFF,(unsigned long)10);
return; return;
} }
...@@ -64,8 +64,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value, ...@@ -64,8 +64,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(unsigned char * /*[10]*/ dest) void uchars(unsigned char * /*[10]*/ dest)
{ {
unsigned char *res = unsigned char *res =
memset_uchar(dest,(unsigned char)0xFF,(unsigned int)10); memset_uchar(dest,(unsigned char)0xFF,(unsigned long)10);
memset_uchar(res,(unsigned char)0xFF,(unsigned int)10); memset_uchar(res,(unsigned char)0xFF,(unsigned long)10);
return; return;
} }
...@@ -92,8 +92,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10] ...@@ -92,8 +92,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (* /*[10]*/ dest)[10]) void nested_chars(char (* /*[10]*/ dest)[10])
{ {
char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned int)100); char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned long)100);
memset_arr10_char(res,(char)0xFF,(unsigned int)100); memset_arr10_char(res,(char)0xFF,(unsigned long)100);
return; return;
} }
...@@ -118,8 +118,8 @@ int *memset_int_FF(int *ptr, size_t len) ...@@ -118,8 +118,8 @@ int *memset_int_FF(int *ptr, size_t len)
void integer(int * /*[10]*/ dest) void integer(int * /*[10]*/ dest)
{ {
int *res = memset_int_FF(dest,(unsigned int)10 * sizeof(int)); int *res = memset_int_FF(dest,(unsigned long)10 * sizeof(int));
memset_int_FF(res,(unsigned int)10 * sizeof(int)); memset_int_FF(res,(unsigned long)10 * sizeof(int));
return; return;
} }
...@@ -144,8 +144,8 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len) ...@@ -144,8 +144,8 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len)
void with_enum(enum E * /*[10]*/ dest) void with_enum(enum E * /*[10]*/ dest)
{ {
enum E *res = memset_e_E_FF(dest,(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 int)10 * sizeof(enum E)); memset_e_E_FF(res,(unsigned long)10 * sizeof(enum E));
return; return;
} }
...@@ -171,21 +171,21 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len) ...@@ -171,21 +171,21 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
void unsigned_integer(unsigned int * /*[10]*/ dest) void unsigned_integer(unsigned int * /*[10]*/ dest)
{ {
unsigned int *res = unsigned int *res =
memset_uint_FF(dest,(unsigned int)10 * sizeof(unsigned int)); memset_uint_FF(dest,(unsigned long)10 * sizeof(unsigned int));
memset_uint_FF(res,(unsigned int)10 * sizeof(unsigned int)); memset_uint_FF(res,(unsigned long)10 * sizeof(unsigned int));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 ensures
set_content: set_content:
\let __fc_len = len / 4; \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((long)0); ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ ~((long)0);
ensures result: \result ≡ ptr; ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 4 - 1)), \result; assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr; assigns \result \from ptr;
*/ */
long *memset_long_FF(long *ptr, size_t len) long *memset_long_FF(long *ptr, size_t len)
...@@ -197,21 +197,22 @@ 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) void long_integer(long * /*[10]*/ dest)
{ {
long *res = memset_long_FF(dest,(unsigned int)10 * sizeof(long)); long *res = memset_long_FF(dest,(unsigned long)10 * sizeof(long));
memset_long_FF(res,(unsigned int)10 * sizeof(long)); memset_long_FF(res,(unsigned long)10 * sizeof(long));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 ensures
set_content: set_content:
\let __fc_len = len / 4; \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 4294967295; ∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(ptr + j0) ≡ 18446744073709551615;
ensures result: \result ≡ ptr; ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 4 - 1)), \result; assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr; assigns \result \from ptr;
*/ */
unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len) 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) ...@@ -224,8 +225,8 @@ unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
void unsigned_long_integer(unsigned long * /*[10]*/ dest) void unsigned_long_integer(unsigned long * /*[10]*/ dest)
{ {
unsigned long *res = unsigned long *res =
memset_ulong_FF(dest,(unsigned int)10 * sizeof(unsigned long)); memset_ulong_FF(dest,(unsigned long)10 * sizeof(unsigned long));
memset_ulong_FF(res,(unsigned int)10 * sizeof(unsigned long)); memset_ulong_FF(res,(unsigned long)10 * sizeof(unsigned long));
return; return;
} }
...@@ -251,8 +252,8 @@ long long *memset_llong_FF(long long *ptr, size_t len) ...@@ -251,8 +252,8 @@ long long *memset_llong_FF(long long *ptr, size_t len)
void long_long_integer(long long * /*[10]*/ dest) void long_long_integer(long long * /*[10]*/ dest)
{ {
long long *res = long long *res =
memset_llong_FF(dest,(unsigned int)10 * sizeof(long long)); memset_llong_FF(dest,(unsigned long)10 * sizeof(long long));
memset_llong_FF(res,(unsigned int)10 * sizeof(long long)); memset_llong_FF(res,(unsigned long)10 * sizeof(long long));
return; return;
} }
...@@ -279,8 +280,8 @@ unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len) ...@@ -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) void unsigned_long_long_integer(unsigned long long * /*[10]*/ dest)
{ {
unsigned long long *res = unsigned long long *res =
memset_ullong_FF(dest,(unsigned int)10 * sizeof(unsigned long long)); memset_ullong_FF(dest,(unsigned long)10 * sizeof(unsigned long long));
memset_ullong_FF(res,(unsigned int)10 * sizeof(unsigned long long)); memset_ullong_FF(res,(unsigned long)10 * sizeof(unsigned long long));
return; return;
} }
...@@ -305,15 +306,15 @@ float *memset_float_FF(float *ptr, size_t len) ...@@ -305,15 +306,15 @@ float *memset_float_FF(float *ptr, size_t len)
void floats(float * /*[10]*/ dest) void floats(float * /*[10]*/ dest)
{ {
float *res = memset_float_FF(dest,(unsigned int)10 * sizeof(float)); float *res = memset_float_FF(dest,(unsigned long)10 * sizeof(float));
memset_float_FF(res,(unsigned int)10 * sizeof(float)); memset_float_FF(res,(unsigned long)10 * sizeof(float));
return; return;
} }
void with_named(named * /*[10]*/ dest) void with_named(named * /*[10]*/ dest)
{ {
named *res = memset_int_FF(dest,(unsigned int)10 * sizeof(named)); named *res = memset_int_FF(dest,(unsigned long)10 * sizeof(named));
memset_int_FF(res,(unsigned int)10 * sizeof(named)); memset_int_FF(res,(unsigned long)10 * sizeof(named));
return; return;
} }
...@@ -340,21 +341,21 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len) ...@@ -340,21 +341,21 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len)
void structure(struct X * /*[10]*/ dest) void structure(struct X * /*[10]*/ dest)
{ {
struct X *res = memset_st_X_FF(dest,(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 int)10 * sizeof(struct X)); memset_st_X_FF(res,(unsigned long)10 * sizeof(struct X));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 ensures
set_content: set_content:
\let __fc_len = len / 4; \let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(ptr + j0)); ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(ptr + j0));
ensures result: \result ≡ ptr; ensures result: \result ≡ ptr;
assigns *(ptr + (0 .. len / 4 - 1)), \result; assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr; assigns \result \from ptr;
*/ */
int **memset_ptr_int_FF(int **ptr, size_t len) int **memset_ptr_int_FF(int **ptr, size_t len)
...@@ -366,8 +367,8 @@ 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) void pointers(int ** /*[10]*/ dest)
{ {
int **res = memset_ptr_int_FF(dest,(unsigned int)10 * sizeof(int *)); int **res = memset_ptr_int_FF(dest,(unsigned long)10 * sizeof(int *));
memset_ptr_int_FF(res,(unsigned int)10 * sizeof(int *)); memset_ptr_int_FF(res,(unsigned long)10 * sizeof(int *));
return; return;
} }
...@@ -395,22 +396,22 @@ int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10] ...@@ -395,22 +396,22 @@ int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10]
void nested(int (*dest)[10], int n) void nested(int (*dest)[10], int n)
{ {
int (*res)[10] = int (*res)[10] =
memset_arr10_int_FF(dest,(unsigned int)n * sizeof(int [10])); memset_arr10_int_FF(dest,(unsigned long)n * sizeof(int [10]));
memset_arr10_int_FF(res,(unsigned int)n * sizeof(int [10])); memset_arr10_int_FF(res,(unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *dest) void with_void(void *dest)
{ {
void *res = memset(dest,0xFF,(unsigned int)10); void *res = memset(dest,0xFF,(unsigned long)10);
memset(res,0xFF,(unsigned int)10); memset(res,0xFF,(unsigned long)10);
return; return;
} }
void with_null_or_int(void) void with_null_or_int(void)
{ {
memset((void *)0,0xFF,(unsigned int)10); memset((void *)0,0xFF,(unsigned long)10);
memset((void *)((int *)42),0xFF,(unsigned int)10); memset((void *)((int *)42),0xFF,(unsigned long)10);
return; return;
} }
...@@ -450,8 +451,8 @@ char *memset_char(char *ptr, char value, size_t len) ...@@ -450,8 +451,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char *dest) void chars(char *dest)
{ {
char *res = memset_char(dest,(char)0xFF,(unsigned int)10); char *res = memset_char(dest,(char)0xFF,(unsigned long)10);
memset_char(res,(char)0xFF,(unsigned int)10); memset_char(res,(char)0xFF,(unsigned long)10);
return; return;
} }
...@@ -477,8 +478,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value, ...@@ -477,8 +478,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(unsigned char *dest) void uchars(unsigned char *dest)
{ {
unsigned char *res = unsigned char *res =
memset_uchar(dest,(unsigned char)0xFF,(unsigned int)10); memset_uchar(dest,(unsigned char)0xFF,(unsigned long)10);
memset_uchar(res,(unsigned char)0xFF,(unsigned int)10); memset_uchar(res,(unsigned char)0xFF,(unsigned long)10);
return; return;
} }
...@@ -506,8 +507,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10] ...@@ -506,8 +507,8 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10]
void nested_chars(char (*dest)[10]) void nested_chars(char (*dest)[10])
{ {
char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned int)100); char (*res)[10] = memset_arr10_char(dest,(char)0xFF,(unsigned long)100);
memset_arr10_char(res,(char)0xFF,(unsigned int)100); memset_arr10_char(res,(char)0xFF,(unsigned long)100);
return; return;
} }
...@@ -532,8 +533,8 @@ int *memset_int_FF(int *ptr, size_t len) ...@@ -532,8 +533,8 @@ int *memset_int_FF(int *ptr, size_t len)
void integer(int *dest) void integer(int *dest)
{ {
int *res = memset_int_FF(dest,(unsigned int)10 * sizeof(int)); int *res = memset_int_FF(dest,(unsigned long)10 * sizeof(int));
memset_int_FF(res,(unsigned int)10 * sizeof(int)); memset_int_FF(res,(unsigned long)10 * sizeof(int));
return; return;
} }
...@@ -558,8 +559,8 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len) ...@@ -558,8 +559,8 @@ enum E *memset_e_E_FF(enum E *ptr, size_t len)
void with_enum(enum E *dest) void with_enum(enum E *dest)
{ {
enum E *res = memset_e_E_FF(dest,(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 int)10 * sizeof(enum E)); memset_e_E_FF(res,(unsigned long)10 * sizeof(enum E));
return; return;
} }
...@@ -585,21 +586,21 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len) ...@@ -585,21 +586,21 @@ unsigned int *memset_uint_FF(unsigned int *ptr, size_t len)
void unsigned_integer(unsigned int *dest) void unsigned_integer(unsigned int *dest)
{ {
unsigned int *res = unsigned int *res =
memset_uint_FF(dest,(unsigned int)10 * sizeof(unsigned int)); memset_uint_FF(dest,(unsigned long)10 * sizeof(unsigned int));
memset_uint_FF(res,(unsigned int)10 * sizeof(unsigned int)); memset_uint_FF(res,(unsigned long)10 * sizeof(unsigned int));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 ensures
set_content: set_content:
\let __fc_len = \old(len) / 4; \let __fc_len = \old(len) / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((long)0); ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ ~((long)0);
ensures result: \result ≡ \old(ptr); ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 4 - 1)), \result; assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr; assigns \result \from ptr;
*/ */
long *memset_long_FF(long *ptr, size_t len) long *memset_long_FF(long *ptr, size_t len)
...@@ -611,21 +612,22 @@ 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) void long_integer(long *dest)
{ {
long *res = memset_long_FF(dest,(unsigned int)10 * sizeof(long)); long *res = memset_long_FF(dest,(unsigned long)10 * sizeof(long));
memset_long_FF(res,(unsigned int)10 * sizeof(long)); memset_long_FF(res,(unsigned long)10 * sizeof(long));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 ensures
set_content: set_content:
\let __fc_len = \old(len) / 4; \let __fc_len = \old(len) / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 4294967295; ∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(\old(ptr) + j0) ≡ 18446744073709551615;
ensures result: \result ≡ \old(ptr); ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 4 - 1)), \result; assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr; assigns \result \from ptr;
*/ */
unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len) 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) ...@@ -638,8 +640,8 @@ unsigned long *memset_ulong_FF(unsigned long *ptr, size_t len)
void unsigned_long_integer(unsigned long *dest) void unsigned_long_integer(unsigned long *dest)
{ {
unsigned long *res = unsigned long *res =
memset_ulong_FF(dest,(unsigned int)10 * sizeof(unsigned long)); memset_ulong_FF(dest,(unsigned long)10 * sizeof(unsigned long));
memset_ulong_FF(res,(unsigned int)10 * sizeof(unsigned long)); memset_ulong_FF(res,(unsigned long)10 * sizeof(unsigned long));
return; return;
} }
...@@ -666,8 +668,8 @@ long long *memset_llong_FF(long long *ptr, size_t len) ...@@ -666,8 +668,8 @@ long long *memset_llong_FF(long long *ptr, size_t len)
void long_long_integer(long long *dest) void long_long_integer(long long *dest)
{ {
long long *res = long long *res =
memset_llong_FF(dest,(unsigned int)10 * sizeof(long long)); memset_llong_FF(dest,(unsigned long)10 * sizeof(long long));
memset_llong_FF(res,(unsigned int)10 * sizeof(long long)); memset_llong_FF(res,(unsigned long)10 * sizeof(long long));
return; return;
} }
...@@ -694,8 +696,8 @@ unsigned long long *memset_ullong_FF(unsigned long long *ptr, size_t len) ...@@ -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) void unsigned_long_long_integer(unsigned long long *dest)
{ {
unsigned long long *res = unsigned long long *res =
memset_ullong_FF(dest,(unsigned int)10 * sizeof(unsigned long long)); memset_ullong_FF(dest,(unsigned long)10 * sizeof(unsigned long long));
memset_ullong_FF(res,(unsigned int)10 * sizeof(unsigned long long)); memset_ullong_FF(res,(unsigned long)10 * sizeof(unsigned long long));
return; return;
} }
...@@ -720,15 +722,15 @@ float *memset_float_FF(float *ptr, size_t len) ...@@ -720,15 +722,15 @@ float *memset_float_FF(float *ptr, size_t len)
void floats(float *dest) void floats(float *dest)
{ {
float *res = memset_float_FF(dest,(unsigned int)10 * sizeof(float)); float *res = memset_float_FF(dest,(unsigned long)10 * sizeof(float));
memset_float_FF(res,(unsigned int)10 * sizeof(float)); memset_float_FF(res,(unsigned long)10 * sizeof(float));
return; return;
} }
void with_named(named *dest) void with_named(named *dest)
{ {
named *res = memset_int_FF(dest,(unsigned int)10 * sizeof(named)); named *res = memset_int_FF(dest,(unsigned long)10 * sizeof(named));
memset_int_FF(res,(unsigned int)10 * sizeof(named)); memset_int_FF(res,(unsigned long)10 * sizeof(named));
return; return;
} }
...@@ -756,21 +758,21 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len) ...@@ -756,21 +758,21 @@ struct X *memset_st_X_FF(struct X *ptr, size_t len)
void structure(struct X *dest) void structure(struct X *dest)
{ {
struct X *res = memset_st_X_FF(dest,(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 int)10 * sizeof(struct X)); memset_st_X_FF(res,(unsigned long)10 * sizeof(struct X));
return; return;
} }
/*@ requires aligned_end: len % 4 ≡ 0; /*@ requires aligned_end: len % 8 ≡ 0;
requires 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 ensures
set_content: set_content:
\let __fc_len = \old(len) / 4; \let __fc_len = \old(len) / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(\old(ptr) + j0)); ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ ¬\valid_read(*(\old(ptr) + j0));
ensures result: \result ≡ \old(ptr); ensures result: \result ≡ \old(ptr);
assigns *(ptr + (0 .. len / 4 - 1)), \result; assigns *(ptr + (0 .. len / 8 - 1)), \result;
assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; assigns *(ptr + (0 .. len / 8 - 1)) \from \nothing;
assigns \result \from ptr; assigns \result \from ptr;
*/ */
int **memset_ptr_int_FF(int **ptr, size_t len) int **memset_ptr_int_FF(int **ptr, size_t len)
...@@ -782,8 +784,8 @@ 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) void pointers(int **dest)
{ {
int **res = memset_ptr_int_FF(dest,(unsigned int)10 * sizeof(int *)); int **res = memset_ptr_int_FF(dest,(unsigned long)10 * sizeof(int *));
memset_ptr_int_FF(res,(unsigned int)10 * sizeof(int *)); memset_ptr_int_FF(res,(unsigned long)10 * sizeof(int *));
return; return;
} }
...@@ -812,22 +814,22 @@ int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10] ...@@ -812,22 +814,22 @@ int (*memset_arr10_int_FF(int (*ptr)[10], size_t len))[10]
void nested(int (*dest)[10], int n) void nested(int (*dest)[10], int n)
{ {
int (*res)[10] = int (*res)[10] =
memset_arr10_int_FF(dest,(unsigned int)n * sizeof(int [10])); memset_arr10_int_FF(dest,(unsigned long)n * sizeof(int [10]));
memset_arr10_int_FF(res,(unsigned int)n * sizeof(int [10])); memset_arr10_int_FF(res,(unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *dest) void with_void(void *dest)
{ {
void *res = memset(dest,0xFF,(unsigned int)10); void *res = memset(dest,0xFF,(unsigned long)10);
memset(res,0xFF,(unsigned int)10); memset(res,0xFF,(unsigned long)10);
return; return;
} }
void with_null_or_int(void) void with_null_or_int(void)
{ {
memset((void *)0,0xFF,(unsigned int)10); memset((void *)0,0xFF,(unsigned long)10);
memset((void *)((int *)42),0xFF,(unsigned int)10); memset((void *)((int *)42),0xFF,(unsigned long)10);
return; return;
} }
......
src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+ 50
− 48
View file @ 11d48df2
...@@ -68,8 +68,8 @@ char *memset_char(char *ptr, char value, size_t len) ...@@ -68,8 +68,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char * /*[10]*/ dest, char value) void chars(char * /*[10]*/ dest, char value)
{ {
char *res = memset_char(dest,value,(unsigned int)10); char *res = memset_char(dest,value,(unsigned long)10);
memset_char(res,value,(unsigned int)10); memset_char(res,value,(unsigned long)10);
return; return;
} }
...@@ -92,8 +92,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value, ...@@ -92,8 +92,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(char * /*[10]*/ dest, unsigned char value) void uchars(char * /*[10]*/ dest, unsigned char value)
{ {
unsigned char *res = memset_char(dest,(char)value,(unsigned int)10); unsigned char *res = memset_char(dest,(char)value,(unsigned long)10);
memset_uchar(res,value,(unsigned int)10); memset_uchar(res,value,(unsigned long)10);
return; return;
} }
...@@ -120,73 +120,74 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10] ...@@ -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) void nested_chars(char (* /*[10]*/ dest)[10], char value)
{ {
char (*res)[10] = memset_arr10_char(dest,value,(unsigned int)100); char (*res)[10] = memset_arr10_char(dest,value,(unsigned long)100);
memset_arr10_char(res,value,(unsigned int)100); memset_arr10_char(res,value,(unsigned long)100);
return; return;
} }
void integer(int * /*[10]*/ dest, int value) void integer(int * /*[10]*/ dest, int value)
{ {
int *res = memset((void *)dest,value,(unsigned int)10 * sizeof(int)); int *res = memset((void *)dest,value,(unsigned long)10 * sizeof(int));
memset((void *)res,value,(unsigned int)10 * sizeof(int)); memset((void *)res,value,(unsigned long)10 * sizeof(int));
return; return;
} }
void with_enum(enum E * /*[10]*/ dest, int value) void with_enum(enum E * /*[10]*/ dest, int value)
{ {
enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E)); enum E *res =
memset((void *)res,value,(unsigned int)10 * sizeof(enum E)); memset((void *)dest,value,(unsigned long)10 * sizeof(enum E));
memset((void *)res,value,(unsigned long)10 * sizeof(enum E));
return; return;
} }
void with_named(named * /*[10]*/ dest, int value) void with_named(named * /*[10]*/ dest, int value)
{ {
named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named)); named *res = memset((void *)dest,value,(unsigned long)10 * sizeof(named));
memset((void *)res,value,(unsigned int)10 * sizeof(named)); memset((void *)res,value,(unsigned long)10 * sizeof(named));
return; return;
} }
void structure(struct X * /*[10]*/ dest, int value) void structure(struct X * /*[10]*/ dest, int value)
{ {
struct X *res = struct X *res =
memset((void *)dest,value,(unsigned int)10 * sizeof(struct X)); memset((void *)dest,value,(unsigned long)10 * sizeof(struct X));
memset((void *)res,value,(unsigned int)10 * sizeof(struct X)); memset((void *)res,value,(unsigned long)10 * sizeof(struct X));
return; return;
} }
void pointers(int ** /*[10]*/ dest, int value) void pointers(int ** /*[10]*/ dest, int value)
{ {
int **res = memset((void *)dest,value,(unsigned int)10 * sizeof(int *)); int **res = memset((void *)dest,value,(unsigned long)10 * sizeof(int *));
memset((void *)res,value,(unsigned int)10 * sizeof(int *)); memset((void *)res,value,(unsigned long)10 * sizeof(int *));
return; return;
} }
void nested(int (*dest)[10], int n, int value) void nested(int (*dest)[10], int n, int value)
{ {
int (*res)[10] = int (*res)[10] =
memset((void *)dest,value,(unsigned int)n * sizeof(int [10])); memset((void *)dest,value,(unsigned long)n * sizeof(int [10]));
memset((void *)res,value,(unsigned int)n * sizeof(int [10])); memset((void *)res,value,(unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *dest, int value) void with_void(void *dest, int value)
{ {
void *res = memset(dest,value,(unsigned int)10); void *res = memset(dest,value,(unsigned long)10);
memset(res,value,(unsigned int)10); memset(res,value,(unsigned long)10);
return; return;
} }
void with_incomplete(struct incomplete *dest, int value) void with_incomplete(struct incomplete *dest, int value)
{ {
struct incomplete *res = memset((void *)dest,value,(unsigned int)10); struct incomplete *res = memset((void *)dest,value,(unsigned long)10);
memset((void *)res,value,(unsigned int)10); memset((void *)res,value,(unsigned long)10);
return; return;
} }
void with_null_or_int(int value) void with_null_or_int(int value)
{ {
memset((void *)0,value,(unsigned int)10); memset((void *)0,value,(unsigned long)10);
memset((void *)((int *)42),value,(unsigned int)10); memset((void *)((int *)42),value,(unsigned long)10);
return; return;
} }
...@@ -227,8 +228,8 @@ char *memset_char(char *ptr, char value, size_t len) ...@@ -227,8 +228,8 @@ char *memset_char(char *ptr, char value, size_t len)
void chars(char *dest, char value) void chars(char *dest, char value)
{ {
char *res = memset_char(dest,value,(unsigned int)10); char *res = memset_char(dest,value,(unsigned long)10);
memset_char(res,value,(unsigned int)10); memset_char(res,value,(unsigned long)10);
return; return;
} }
...@@ -253,8 +254,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value, ...@@ -253,8 +254,8 @@ unsigned char *memset_uchar(unsigned char *ptr, unsigned char value,
void uchars(char *dest, unsigned char value) void uchars(char *dest, unsigned char value)
{ {
unsigned char *res = memset_char(dest,(char)value,(unsigned int)10); unsigned char *res = memset_char(dest,(char)value,(unsigned long)10);
memset_uchar(res,value,(unsigned int)10); memset_uchar(res,value,(unsigned long)10);
return; return;
} }
...@@ -282,73 +283,74 @@ char (*memset_arr10_char(char (*ptr)[10], char value, size_t len))[10] ...@@ -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) void nested_chars(char (*dest)[10], char value)
{ {
char (*res)[10] = memset_arr10_char(dest,value,(unsigned int)100); char (*res)[10] = memset_arr10_char(dest,value,(unsigned long)100);
memset_arr10_char(res,value,(unsigned int)100); memset_arr10_char(res,value,(unsigned long)100);
return; return;
} }
void integer(int *dest, int value) void integer(int *dest, int value)
{ {
int *res = memset((void *)dest,value,(unsigned int)10 * sizeof(int)); int *res = memset((void *)dest,value,(unsigned long)10 * sizeof(int));
memset((void *)res,value,(unsigned int)10 * sizeof(int)); memset((void *)res,value,(unsigned long)10 * sizeof(int));
return; return;
} }
void with_enum(enum E *dest, int value) void with_enum(enum E *dest, int value)
{ {
enum E *res = memset((void *)dest,value,(unsigned int)10 * sizeof(enum E)); enum E *res =
memset((void *)res,value,(unsigned int)10 * sizeof(enum E)); memset((void *)dest,value,(unsigned long)10 * sizeof(enum E));
memset((void *)res,value,(unsigned long)10 * sizeof(enum E));
return; return;
} }
void with_named(named *dest, int value) void with_named(named *dest, int value)
{ {
named *res = memset((void *)dest,value,(unsigned int)10 * sizeof(named)); named *res = memset((void *)dest,value,(unsigned long)10 * sizeof(named));
memset((void *)res,value,(unsigned int)10 * sizeof(named)); memset((void *)res,value,(unsigned long)10 * sizeof(named));
return; return;
} }
void structure(struct X *dest, int value) void structure(struct X *dest, int value)
{ {
struct X *res = struct X *res =
memset((void *)dest,value,(unsigned int)10 * sizeof(struct X)); memset((void *)dest,value,(unsigned long)10 * sizeof(struct X));
memset((void *)res,value,(unsigned int)10 * sizeof(struct X)); memset((void *)res,value,(unsigned long)10 * sizeof(struct X));
return; return;
} }
void pointers(int **dest, int value) void pointers(int **dest, int value)
{ {
int **res = memset((void *)dest,value,(unsigned int)10 * sizeof(int *)); int **res = memset((void *)dest,value,(unsigned long)10 * sizeof(int *));
memset((void *)res,value,(unsigned int)10 * sizeof(int *)); memset((void *)res,value,(unsigned long)10 * sizeof(int *));
return; return;
} }
void nested(int (*dest)[10], int n, int value) void nested(int (*dest)[10], int n, int value)
{ {
int (*res)[10] = int (*res)[10] =
memset((void *)dest,value,(unsigned int)n * sizeof(int [10])); memset((void *)dest,value,(unsigned long)n * sizeof(int [10]));
memset((void *)res,value,(unsigned int)n * sizeof(int [10])); memset((void *)res,value,(unsigned long)n * sizeof(int [10]));
return; return;
} }
void with_void(void *dest, int value) void with_void(void *dest, int value)
{ {
void *res = memset(dest,value,(unsigned int)10); void *res = memset(dest,value,(unsigned long)10);
memset(res,value,(unsigned int)10); memset(res,value,(unsigned long)10);
return; return;
} }
void with_incomplete(struct incomplete *dest, int value) void with_incomplete(struct incomplete *dest, int value)
{ {
struct incomplete *res = memset((void *)dest,value,(unsigned int)10); struct incomplete *res = memset((void *)dest,value,(unsigned long)10);
memset((void *)res,value,(unsigned int)10); memset((void *)res,value,(unsigned long)10);
return; return;
} }
void with_null_or_int(int value) void with_null_or_int(int value)
{ {
memset((void *)0,value,(unsigned int)10); memset((void *)0,value,(unsigned long)10);
memset((void *)((int *)42),value,(unsigned int)10); memset((void *)((int *)42),value,(unsigned long)10);
return; return;
} }
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment