Newer
Older
[kernel] Parsing tests/string/memcpy.c (with preprocessing)
[instantiate] tests/string/memcpy.c:36: Warning: Ignore call: not well typed
[instantiate] tests/string/memcpy.c:37: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
#include "strings.h"
struct X {
int x ;
int y ;
};
typedef int named;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
requires
separation:
\let __fc_len = len / 4;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
ensures result: \result ≡ dest;
assigns *(dest + (0 .. len / 4 - 1)), \result;
assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int *memcpy_int(int *dest, int const *src, size_t len)
{
int *__retres;
__retres = (int *)memcpy((void *)dest,(void const *)src,len);
return __retres;
}
void integer(int * /*[10]*/ src, int * /*[10]*/ dest)
int *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(int));
memcpy_int(src,res,(unsigned int)10 * sizeof(int));
return;
}
void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
{
named *res = memcpy_int(dest,src,(unsigned int)10 * sizeof(named));
memcpy_int(src,res,(unsigned int)10 * sizeof(named));
return;
}
/*@ requires aligned_end: len % 8 ≡ 0;
requires
valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
requires
separation:
\let __fc_len = len / 8;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 8;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
ensures result: \result ≡ dest;
assigns *(dest + (0 .. len / 8 - 1)), \result;
assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
{
struct X *__retres;
__retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
return __retres;
}
void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
{
struct X *res = memcpy_st_X(dest,src,(unsigned int)10 * sizeof(struct X));
memcpy_st_X(src,res,(unsigned int)10 * sizeof(struct X));
return;
}
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
requires
separation:
\let __fc_len = len / 4;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(dest + j0) ≡ *(src + j0);
ensures result: \result ≡ dest;
assigns *(dest + (0 .. len / 4 - 1)), \result;
assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
{
int **__retres;
__retres = (int **)memcpy((void *)dest,(void const *)src,len);
return __retres;
}
void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
{
int **res = memcpy_ptr_int(dest,src,(unsigned int)10 * sizeof(int *));
memcpy_ptr_int(src,res,(unsigned int)10 * sizeof(int *));
return;
}
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
\let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
requires
separation:
\let __fc_len = len / 40;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
0 ≤ j1 < 10 ⇒ (*(dest + j0))[j1] ≡ (*(src + j0))[j1]);
ensures result: \result ≡ dest;
assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1]
\from (*(src + (0 .. len / 40 - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
{
int (*__retres)[10];
__retres = (int (*)[10])memcpy((void *)dest,(void const *)src,len);
return __retres;
}
void nested(int (*src)[10], int (*dest)[10], int n)
int (*res)[10] =
memcpy_arr10_int(dest,src,(unsigned int)n * sizeof(int [10]));
memcpy_arr10_int(src,res,(unsigned int)n * sizeof(int [10]));
return;
}
void with_void(void *src, void *dest, int n)
{
void *res = memcpy(dest,(void const *)src,(unsigned int)n);
memcpy(src,(void const *)res,(unsigned int)n);
return;
}
[kernel] Parsing tests/string/result/memcpy.c (with preprocessing)
[kernel] Parsing tests/string/memcpy.c (with preprocessing)
[kernel] tests/string/memcpy.c:10: Warning:
dropping duplicate def'n of func integer at tests/string/memcpy.c:10 in favor of that at tests/string/result/memcpy.c:36
[kernel] tests/string/memcpy.c:15: Warning:
dropping duplicate def'n of func with_named at tests/string/memcpy.c:15 in favor of that at tests/string/result/memcpy.c:43
[kernel] tests/string/memcpy.c:20: Warning:
dropping duplicate def'n of func structure at tests/string/memcpy.c:20 in favor of that at tests/string/result/memcpy.c:76
[kernel] tests/string/memcpy.c:25: Warning:
dropping duplicate def'n of func pointers at tests/string/memcpy.c:25 in favor of that at tests/string/result/memcpy.c:109
[kernel] tests/string/memcpy.c:30: Warning:
dropping duplicate def'n of func nested at tests/string/memcpy.c:30 in favor of that at tests/string/result/memcpy.c:147
[kernel] tests/string/memcpy.c:35: Warning:
dropping duplicate def'n of func with_void at tests/string/memcpy.c:35 in favor of that at tests/string/result/memcpy.c:155
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
#include "strings.h"
struct X {
int x ;
int y ;
};
typedef int named;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
requires
separation:
\let __fc_len = len / 4;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 4;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
ensures result: \result ≡ \old(dest);
assigns *(dest + (0 .. len / 4 - 1)), \result;
assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int *memcpy_int(int *dest, int const *src, size_t len)
{
int *__retres;
__retres = (int *)memcpy((void *)dest,(void const *)src,len);
return __retres;
}
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
void integer(int *src, int *dest)
{
int *res =
memcpy_int(dest,(int const *)src,(unsigned int)10 * sizeof(int));
memcpy_int(src,(int const *)res,(unsigned int)10 * sizeof(int));
return;
}
void with_named(named *src, named *dest)
{
named *res =
memcpy_int(dest,(int const *)src,(unsigned int)10 * sizeof(named));
memcpy_int(src,(int const *)res,(unsigned int)10 * sizeof(named));
return;
}
/*@ requires aligned_end: len % 8 ≡ 0;
requires
valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
requires
separation:
\let __fc_len = len / 8;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 8;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
ensures result: \result ≡ \old(dest);
assigns *(dest + (0 .. len / 8 - 1)), \result;
assigns *(dest + (0 .. len / 8 - 1)) \from *(src + (0 .. len / 8 - 1));
struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
{
struct X *__retres;
__retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
return __retres;
}
void structure(struct X *src, struct X *dest)
{
struct X *res =
memcpy_st_X(dest,(struct X const *)src,
(unsigned int)10 * sizeof(struct X));
memcpy_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
return;
}
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
requires
separation:
\let __fc_len = len / 4;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 4;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒ *(\old(dest) + j0) ≡ *(\old(src) + j0);
ensures result: \result ≡ \old(dest);
assigns *(dest + (0 .. len / 4 - 1)), \result;
assigns *(dest + (0 .. len / 4 - 1)) \from *(src + (0 .. len / 4 - 1));
assigns \result \from dest;
*/
int **memcpy_ptr_int(int **dest, int * const *src, size_t len)
int **__retres;
__retres = (int **)memcpy((void *)dest,(void const *)src,len);
return __retres;
}
void pointers(int **src, int **dest)
{
int **res =
memcpy_ptr_int(dest,(int * const *)src,(unsigned int)10 * sizeof(int *));
memcpy_ptr_int(src,(int * const *)res,(unsigned int)10 * sizeof(int *));
return;
}
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
\let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
requires
separation:
\let __fc_len = len / 40;
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
0 ≤ j1 < 10 ⇒
(*(\old(dest) + j0))[j1] ≡ (*(\old(src) + j0))[j1]);
ensures result: \result ≡ \old(dest);
assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1], \result;
assigns (*(dest + (0 .. len / 40 - 1)))[0 .. 10 - 1]
\from (*(src + (0 .. len / 40 - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
{
int (*__retres)[10];
__retres = (int (*)[10])memcpy((void *)dest,(void const *)src,len);
return __retres;
}
void nested(int (*src)[10], int (*dest)[10], int n)
int (*res)[10] =
memcpy_arr10_int(dest,(int const (*)[10])src,
(unsigned int)n * sizeof(int [10]));
memcpy_arr10_int(src,(int const (*)[10])res,
(unsigned int)n * sizeof(int [10]));
void with_void(void *src, void *dest, int n)
{
void *res = memcpy(dest,(void const *)src,(unsigned int)n);
memcpy(src,(void const *)res,(unsigned int)n);
return;
}