Extend.res.oracle

[kernel] Parsing tests/spec/Extend.i (no preprocessing)
[kernel:annot-error] tests/spec/Extend.i:31: Warning: unexpected token 'baz'
[kernel] Reparsing file
/* Generated by Frama-C */
int f(int x);

/*@ behavior test:
      foo y ≡ 1;
      bar \old(y) + \result ≡ 0;
      bla \trace(3) ∧ \trace(2);
 */
int g(int y);

/*@ foo x ≡ 0;
    bar \result ≡ 0;
    bla \trace(6) ∨ \trace(5); */
int f(int x)
{
  int s = 0;
  {
    int i = 0;
    /*@ loop lfoo i ≤ x;
        loop baz \at(i,LoopEntry), 0; */
    while (i < x) {
      int tmp;
      tmp = g(i);
      s += tmp;
      i ++;
    }
  }
  /*@ ca_foo s ≡ 0; */ ;
  return s;
}

int k(int z)
{
  int tmp;
  int x = z;
  int y = 0;
  /*@ ns_foo \at(x,Post) ≡ z + 1; */
  {
    tmp = x;
    x ++;
    y = tmp;
  }
  return y;
}

/*@ global_foo ∀ ℤ x; x < x + 1;
*/
/*@ behavior ca_foo:
      ensures ca_foo: \true; */
void loop(void)
{
  /*@ for ca_foo: ca_foo \true; */ ;
  /*@ ns_foo \true; */
  /*@ baz \true; */
  /*@ loop invariant \true; */
  while (1) break;
  return;
}