memcpy.res.oracle

[kernel] Parsing tests/string/memcpy.c (with preprocessing)
[instantiate] tests/string/memcpy.c:36: Warning: 
  memcpy instantiator cannot replace call
[instantiate] tests/string/memcpy.c:37: Warning: 
  memcpy instantiator cannot replace call
[instantiate] tests/string/memcpy.c:42: Warning: 
  memcpy instantiator cannot replace call
[instantiate] tests/string/memcpy.c:43: Warning: 
  memcpy instantiator cannot replace call
[instantiate] tests/string/memcpy.c:47: Warning: 
  memcpy instantiator cannot replace call
[instantiate] tests/string/memcpy.c:48: Warning: 
  memcpy instantiator cannot replace call
[instantiate] tests/string/memcpy.c:49: Warning: 
  memcpy instantiator cannot replace call
[instantiate] tests/string/memcpy.c:50: Warning: 
  memcpy instantiator cannot replace call
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
#include "strings.h"
struct X {
   int x ;
   int y ;
};
typedef int named;
struct incomplete;
/*@ requires
      separation:
        \let __fc_len = len / 4;
          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
    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));
    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 src[10], int dest[10])
{
  int *res = memcpy_int(dest,src,(unsigned long)10 * sizeof(int));
  memcpy_int(src,res,(unsigned long)10 * sizeof(int));
  return;
}

void with_named(named src[10], named dest[10])
{
  named *res = memcpy_int(dest,src,(unsigned long)10 * sizeof(named));
  memcpy_int(src,res,(unsigned long)10 * sizeof(named));
  return;
}

/*@ requires
      separation:
        \let __fc_len = len / 8;
          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
    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));
    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));
    assigns \result \from dest;
 */
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[10], struct X dest[10])
{
  struct X *res = memcpy_st_X(dest,src,(unsigned long)10 * sizeof(struct X));
  memcpy_st_X(src,res,(unsigned long)10 * sizeof(struct X));
  return;
}

/*@ requires
      separation:
        \let __fc_len = len / 8;
          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
    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));
    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));
    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[10], int *dest[10])
{
  int **res = memcpy_ptr_int(dest,src,(unsigned long)10 * sizeof(int *));
  memcpy_ptr_int(src,res,(unsigned long)10 * sizeof(int *));
  return;
}

/*@ requires
      separation:
        \let __fc_len = len / 40;
          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
    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));
    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 long)n * sizeof(int [10]));
  memcpy_arr10_int(src,res,(unsigned long)n * sizeof(int [10]));
  return;
}

void with_void(void *src, void *dest, int n)
{
  void *res = memcpy(dest,(void const *)src,(unsigned long)n);
  memcpy(src,(void const *)res,(unsigned long)n);
  return;
}

void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
  struct incomplete *res =
    memcpy((void *)dest,(void const *)src,(unsigned long)n);
  memcpy((void *)src,(void const *)res,(unsigned long)n);
  return;
}

void with_null_or_int(int p[10])
{
  memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
  memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
  memcpy((void *)((int *)42),(void const *)p,(unsigned long)10 * sizeof(int));
  memcpy((void *)p,(void const *)((int *)42),(unsigned long)10 * sizeof(int));
  return;
}


[kernel] Parsing tests/string/result/ocode_memcpy.c (with preprocessing)
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
#include "strings.h"
struct X {
   int x ;
   int y ;
};
typedef int named;
struct incomplete;
/*@ requires
      separation:
        \let __fc_len = len / 4;
          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
    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));
    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;
}

void integer(int src[10], int dest[10])
{
  int *res =
    memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(int));
  memcpy_int(src,(int const *)res,(unsigned long)10 * sizeof(int));
  return;
}

void with_named(named src[10], named dest[10])
{
  named *res =
    memcpy_int(dest,(int const *)src,(unsigned long)10 * sizeof(named));
  memcpy_int(src,(int const *)res,(unsigned long)10 * sizeof(named));
  return;
}

/*@ requires
      separation:
        \let __fc_len = len / 8;
          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
    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));
    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));
    assigns \result \from dest;
 */
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[10], struct X dest[10])
{
  struct X *res =
    memcpy_st_X(dest,(struct X const *)src,
                (unsigned long)10 * sizeof(struct X));
  memcpy_st_X(src,(struct X const *)res,(unsigned long)10 * sizeof(struct X));
  return;
}

/*@ requires
      separation:
        \let __fc_len = len / 8;
          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
    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));
    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));
    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[10], int *dest[10])
{
  int **res =
    memcpy_ptr_int(dest,(int * const *)src,(unsigned long)10 * sizeof(int *));
  memcpy_ptr_int(src,(int * const *)res,(unsigned long)10 * sizeof(int *));
  return;
}

/*@ requires
      separation:
        \let __fc_len = len / 40;
          \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
    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));
    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 long)n * sizeof(int [10]));
  memcpy_arr10_int(src,(int const (*)[10])res,
                   (unsigned long)n * sizeof(int [10]));
  return;
}

void with_void(void *src, void *dest, int n)
{
  void *res = memcpy(dest,(void const *)src,(unsigned long)n);
  memcpy(src,(void const *)res,(unsigned long)n);
  return;
}

void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
  struct incomplete *res =
    memcpy((void *)dest,(void const *)src,(unsigned long)n);
  memcpy((void *)src,(void const *)res,(unsigned long)n);
  return;
}

void with_null_or_int(int p[10])
{
  memcpy((void *)0,(void const *)p,(unsigned long)10 * sizeof(int));
  memcpy((void *)p,(void const *)0,(unsigned long)10 * sizeof(int));
  memcpy((void *)((int *)42),(void const *)p,(unsigned long)10 * sizeof(int));
  memcpy((void *)p,(void const *)((int *)42),(unsigned long)10 * sizeof(int));
  return;
}