Commit a5590a85 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/andre/libc-pcpy' into 'master'

synchronize with frama-c/frama-c!3257

See merge request frama-c/frama-clang!151
parents 86747eaf 57b10a76
Pipeline #36447 failed with stages
......@@ -914,6 +914,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
......@@ -564,6 +564,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
......@@ -730,6 +730,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
......@@ -741,6 +741,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
......@@ -745,6 +745,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
......@@ -726,6 +726,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
......@@ -727,6 +727,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
......@@ -641,6 +641,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
......@@ -501,6 +501,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
Markdown is supported
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