add_allocates.res.oracle

[kernel] Parsing add_allocates.i (no preprocessing)
/* Generated by Frama-C */
int *x;
/*@ allocates \nothing; */
void f(void);

/*@ allocates x; */
void g(void);

/*@ allocates \nothing;
    
    behavior b:
      requires \false;
      allocates x; */
void main(int c)
{
  f();
  /*@ loop allocates \nothing; */
  while (c) {
    /*@ loop allocates x; */
    while (1) 
      /*@ loop allocates \nothing; */
      while (! c) ;
    /*@ loop allocates \nothing;
        for b: loop allocates x; */
    while (1) ;
  }
  return;
}