attributes-declarations-definitions.0.res.oracle

[kernel] Parsing attributes-declarations-definitions.c (with preprocessing)
[kernel] attributes-declarations-definitions.c:12: Warning: 
  found two contracts (old location: attributes-declarations-definitions.c:6). Merging them
[kernel] attributes-declarations-definitions.c:21: Warning: 
  found two contracts (old location: attributes-declarations-definitions.c:13). Merging them
/* Generated by Frama-C */
typedef int __attribute__((__a1__)) aint;
typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
(int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
                                                        __f2__, __f1__));

/*@ requires p3 ≥ 3;
    requires p3 ≥ 1;
    requires p3 ≥ 4; */
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
(int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
                                                        __f2__, __f1__));
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
(int const __attribute__((__arg3__)) p3)
{
  int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) __retres;
  __retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p3;
  return __retres;
}

aint g(int __attribute__((__a2__)) i3);

aint g(int __attribute__((__a2__)) i3)
{
  aint __retres;
  __retres = (int __attribute__((__a1__)))i3;
  return __retres;
}

iptr h(iptr volatile ip2);

iptr h(iptr volatile ip2)
{
  iptr __retres;
  __retres = (int __attribute__((__p1__)) *)0;
  return __retres;
}

void test(void)
{
  int a;
  int b __attribute__((__unused__));
  return;
}

int __attribute__((__o__)) one_letter_attribute;
int __attribute__((__n__)) one_letter_attribute_with_underscore;
int __attribute__((__e__)) one_letter_attribute_with_underscore_after;