attributes-declarations-definitions.res.oracle

[kernel] Parsing tests/syntax/attributes-declarations-definitions.c (with preprocessing)
[kernel] tests/syntax/attributes-declarations-definitions.c:7: Warning: 
  found two contracts (old location: tests/syntax/attributes-declarations-definitions.c:1). Merging them
[kernel] tests/syntax/attributes-declarations-definitions.c:16: Warning: 
  found two contracts (old location: tests/syntax/attributes-declarations-definitions.c:8). 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;