memcmp.res.oracle

[kernel] Parsing tests/string/memcmp.c (with preprocessing)
[instantiate] tests/string/memcmp.c:31: Warning: 
  memcmp instantiator cannot replace call
[instantiate] tests/string/memcmp.c:36: Warning: 
  memcmp instantiator cannot replace call
[instantiate] tests/string/memcmp.c:40: Warning: 
  memcmp instantiator cannot replace call
[instantiate] tests/string/memcmp.c:41: Warning: 
  memcmp instantiator cannot replace call
[instantiate] tests/string/memcmp.c:42: Warning: 
  memcmp instantiator cannot replace call
[instantiate] tests/string/memcmp.c:43: Warning: 
  memcmp 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 aligned_end: len % 4 ≡ 0;
    requires
      valid_read_s1:
        \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1));
    requires
      valid_read_s2:
        \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1));
    ensures
      equals:
        \let __fc_len = len / 4;
          \result ≡ 0 ⇔
          (∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 .. len / 4 - 1))),
            (indirect: *(s2 + (0 .. len / 4 - 1)));
 */
int memcmp_int(int const *s1, int const *s2, size_t len)
{
  int __retres;
  __retres = memcmp((void const *)s1,(void const *)s2,len);
  return __retres;
}

int integer(int s1[10], int s2[10])
{
  int tmp;
  tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(int));
  return tmp;
}

int with_named(named s1[10], named s2[10])
{
  int tmp;
  tmp = memcmp_int(s1,s2,(unsigned long)10 * sizeof(named));
  return tmp;
}

/*@ requires aligned_end: len % 8 ≡ 0;
    requires
      valid_read_s1:
        \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
    requires
      valid_read_s2:
        \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
    ensures
      equals:
        \let __fc_len = len / 8;
          \result ≡ 0 ⇔
          (∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 .. len / 8 - 1))),
            (indirect: *(s2 + (0 .. len / 8 - 1)));
 */
int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
{
  int __retres;
  __retres = memcmp((void const *)s1,(void const *)s2,len);
  return __retres;
}

int structure(struct X s1[10], struct X s2[10])
{
  int tmp;
  tmp = memcmp_st_X(s1,s2,(unsigned long)10 * sizeof(struct X));
  return tmp;
}

/*@ requires aligned_end: len % 8 ≡ 0;
    requires
      valid_read_s1:
        \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
    requires
      valid_read_s2:
        \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
    ensures
      equals:
        \let __fc_len = len / 8;
          \result ≡ 0 ⇔
          (∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ *(s1 + j0) ≡ *(s2 + j0));
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 .. len / 8 - 1))),
            (indirect: *(s2 + (0 .. len / 8 - 1)));
 */
int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
{
  int __retres;
  __retres = memcmp((void const *)s1,(void const *)s2,len);
  return __retres;
}

int pointers(int *s1[10], int *s2[10])
{
  int tmp;
  tmp = memcmp_ptr_int(s1,s2,(unsigned long)10 * sizeof(int *));
  return tmp;
}

/*@ requires aligned_end: len % 40 ≡ 0;
    requires
      valid_read_s1:
        \let __fc_len = len / 40; \valid_read(s1 + (0 .. __fc_len - 1));
    requires
      valid_read_s2:
        \let __fc_len = len / 40; \valid_read(s2 + (0 .. __fc_len - 1));
    ensures
      equals:
        \let __fc_len = len / 40;
          \result ≡ 0 ⇔
          (∀ ℤ j0;
             0 ≤ j0 < __fc_len ⇒
             (∀ ℤ j1;
                0 ≤ j1 < 10 ⇒ (*(s1 + j0))[j1] ≡ (*(s2 + j0))[j1]));
    assigns \result;
    assigns \result
      \from (indirect: (*(s1 + (0 .. len / 40 - 1)))[0 .. 10 - 1]),
            (indirect: (*(s2 + (0 .. len / 40 - 1)))[0 .. 10 - 1]);
 */
int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
{
  int __retres;
  __retres = memcmp((void const *)s1,(void const *)s2,len);
  return __retres;
}

int nested(int (*s1)[10], int (*s2)[10], int n)
{
  int tmp;
  tmp = memcmp_arr10_int(s1,s2,(unsigned long)n * sizeof(int [10]));
  return tmp;
}

int with_void(void *s1, void *s2, int n)
{
  int tmp;
  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)10);
  return tmp;
}

int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
{
  int tmp;
  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)n);
  return tmp;
}

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


[kernel] Parsing tests/string/result/ocode_memcmp.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 aligned_end: len % 4 ≡ 0;
    requires
      valid_read_s1:
        \let __fc_len = len / 4; \valid_read(s1 + (0 .. __fc_len - 1));
    requires
      valid_read_s2:
        \let __fc_len = len / 4; \valid_read(s2 + (0 .. __fc_len - 1));
    ensures
      equals:
        \let __fc_len = \old(len) / 4;
          \result ≡ 0 ⇔
          (∀ ℤ j0;
             0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0));
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 .. len / 4 - 1))),
            (indirect: *(s2 + (0 .. len / 4 - 1)));
 */
int memcmp_int(int const *s1, int const *s2, size_t len)
{
  int __retres;
  __retres = memcmp((void const *)s1,(void const *)s2,len);
  return __retres;
}

int integer(int s1[10], int s2[10])
{
  int tmp;
  tmp = memcmp_int((int const *)s1,(int const *)s2,
                   (unsigned long)10 * sizeof(int));
  return tmp;
}

int with_named(named s1[10], named s2[10])
{
  int tmp;
  tmp = memcmp_int((int const *)s1,(int const *)s2,
                   (unsigned long)10 * sizeof(named));
  return tmp;
}

/*@ requires aligned_end: len % 8 ≡ 0;
    requires
      valid_read_s1:
        \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
    requires
      valid_read_s2:
        \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
    ensures
      equals:
        \let __fc_len = \old(len) / 8;
          \result ≡ 0 ⇔
          (∀ ℤ j0;
             0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0));
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 .. len / 8 - 1))),
            (indirect: *(s2 + (0 .. len / 8 - 1)));
 */
int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
{
  int __retres;
  __retres = memcmp((void const *)s1,(void const *)s2,len);
  return __retres;
}

int structure(struct X s1[10], struct X s2[10])
{
  int tmp;
  tmp = memcmp_st_X((struct X const *)s1,(struct X const *)s2,
                    (unsigned long)10 * sizeof(struct X));
  return tmp;
}

/*@ requires aligned_end: len % 8 ≡ 0;
    requires
      valid_read_s1:
        \let __fc_len = len / 8; \valid_read(s1 + (0 .. __fc_len - 1));
    requires
      valid_read_s2:
        \let __fc_len = len / 8; \valid_read(s2 + (0 .. __fc_len - 1));
    ensures
      equals:
        \let __fc_len = \old(len) / 8;
          \result ≡ 0 ⇔
          (∀ ℤ j0;
             0 ≤ j0 < __fc_len ⇒ *(\old(s1) + j0) ≡ *(\old(s2) + j0));
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 .. len / 8 - 1))),
            (indirect: *(s2 + (0 .. len / 8 - 1)));
 */
int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
{
  int __retres;
  __retres = memcmp((void const *)s1,(void const *)s2,len);
  return __retres;
}

int pointers(int *s1[10], int *s2[10])
{
  int tmp;
  tmp = memcmp_ptr_int((int * const *)s1,(int * const *)s2,
                       (unsigned long)10 * sizeof(int *));
  return tmp;
}

/*@ requires aligned_end: len % 40 ≡ 0;
    requires
      valid_read_s1:
        \let __fc_len = len / 40; \valid_read(s1 + (0 .. __fc_len - 1));
    requires
      valid_read_s2:
        \let __fc_len = len / 40; \valid_read(s2 + (0 .. __fc_len - 1));
    ensures
      equals:
        \let __fc_len = \old(len) / 40;
          \result ≡ 0 ⇔
          (∀ ℤ j0;
             0 ≤ j0 < __fc_len ⇒
             (∀ ℤ j1;
                0 ≤ j1 < 10 ⇒
                (*(\old(s1) + j0))[j1] ≡ (*(\old(s2) + j0))[j1]));
    assigns \result;
    assigns \result
      \from (indirect: (*(s1 + (0 .. len / 40 - 1)))[0 .. 10 - 1]),
            (indirect: (*(s2 + (0 .. len / 40 - 1)))[0 .. 10 - 1]);
 */
int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
{
  int __retres;
  __retres = memcmp((void const *)s1,(void const *)s2,len);
  return __retres;
}

int nested(int (*s1)[10], int (*s2)[10], int n)
{
  int tmp;
  tmp = memcmp_arr10_int((int const (*)[10])s1,(int const (*)[10])s2,
                         (unsigned long)n * sizeof(int [10]));
  return tmp;
}

int with_void(void *s1, void *s2, int n)
{
  int tmp;
  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)10);
  return tmp;
}

int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
{
  int tmp;
  tmp = memcmp((void const *)s1,(void const *)s2,(unsigned long)n);
  return tmp;
}

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