assign2.res.oracle

[kernel] Parsing tests/rte/assign2.c (with preprocessing)
[rte] annotating function f
[rte] annotating function main
/* Generated by Frama-C */
int i;
int t[10];
/*@ ensures 0 ≤ \result ≤ 0; */
int any(void);

/*@ ensures t[i] ≡ \old(t[\at(i,Here)]) + 1;
    ensures \let j = i; t[j] ≡ \old(t[j]) + 1;
    assigns i, t[\at(i,Post)];
 */
void f(void)
{
  i = any();
  /*@ assert rte: signed_overflow: t[i] + 1 ≤ 2147483647; */
  (t[i]) ++;
  return;
}

int main(void)
{
  int __retres;
  f();
  f();
  __retres = 0;
  return __retres;
}