declspec.res.oracle

[kernel] Parsing declspec.c (with preprocessing)
/* Generated by Frama-C */
/*@ axiomatic Foo {
      predicate p(char *s) ;
      
      }
 */
/*@ requires p(b); */
void f(char const * __attribute__((__whatever__)) a,
       char * __attribute__((__p__)) b)
{
  /*@ assert p(b); */ ;
  return;
}