attributes-declarations-definitions.0.res.oracle

[kernel] Parsing attributes-declarations-definitions.c (with preprocessing)
[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning: 
  Unknown attribute: tret1
[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning: 
  Unknown attribute: f1
[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning: 
  Unknown attribute: arg1
[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning: 
  Unknown attribute: tret2
[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning: 
  Unknown attribute: f2
[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning: 
  Unknown attribute: arg2
[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning: 
  Unknown attribute: tret3
[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning: 
  Unknown attribute: arg3
[kernel] attributes-declarations-definitions.c:12: Warning: 
  found two contracts (old location: attributes-declarations-definitions.c:6). Merging them
[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning: 
  Unknown attribute: tret4
[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning: 
  Unknown attribute: f4
[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning: 
  Unknown attribute: arg4
[kernel] attributes-declarations-definitions.c:21: Warning: 
  found two contracts (old location: attributes-declarations-definitions.c:13). Merging them
[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning: 
  Unknown attribute: tret5
[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning: 
  Unknown attribute: f5
[kernel:unknown-attribute] attributes-declarations-definitions.c:25: Warning: 
  Unknown attribute: a1
[kernel:unknown-attribute] attributes-declarations-definitions.c:33: Warning: 
  Unknown attribute: a2
[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning: 
  Unknown attribute: p1
[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning: 
  Unknown attribute: p2
[kernel:unknown-attribute] attributes-declarations-definitions.c:56: Warning: 
  Unknown attribute: _n
[kernel:unknown-attribute] attributes-declarations-definitions.c:58: Warning: 
  Unknown attribute: e_
/* 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)
{
  return p3;
}

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

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

iptr h(iptr volatile ip2);

iptr h(iptr volatile ip2)
{
  iptr __retres;
  __retres = (iptr)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;