[kernel] Parsing tests/syntax/Refresh_visitor.i (no preprocessing)
Start
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  
[eva:alarm] tests/syntax/Refresh_visitor.i:17: Warning: 
  assertion got status unknown.
[eva] tests/syntax/Refresh_visitor.i:23: loop invariant got status valid.
[eva] tests/syntax/Refresh_visitor.i:24: loop invariant got status valid.
[eva] tests/syntax/Refresh_visitor.i:29: loop invariant got status valid.
[eva] tests/syntax/Refresh_visitor.i:30: loop invariant got status valid.
[eva] tests/syntax/Refresh_visitor.i:32: starting to merge loop iterations
[eva] tests/syntax/Refresh_visitor.i:26: starting to merge loop iterations
[eva:alarm] tests/syntax/Refresh_visitor.i:14: Warning: 
  function main: postcondition got status unknown.
[eva] Recording results for main
[eva] done for function main
/* Generated by Frama-C */
struct S {
   int i ;
};
struct matrix {
   int m[100] ;
};
/*@ lemma foo: ∀ struct S x; x.i ≥ 0 ∨ x.i < 0;
 */
/*@ ensures \result ≥ \old(x.i); */
int main(struct S x, struct matrix m)
{
  struct matrix m_t;
  int y = x.i;
  /*@ assert y ≡ x.i; */ ;
  int i = 0;
  int j = 0;
  i = 0;
  /*@ loop invariant 0 ≤ i ≤ 2;
      loop invariant 0 ≤ j ≤ 2;
      loop assigns i, j, m_t;
  */
  while (i < 2) {
    j = 0;
    /*@ loop invariant 0 ≤ j ≤ 2;
        loop invariant 0 ≤ i < 2;
        loop assigns j, m_t;
    */
    while (j < 2) {
      m_t.m[i * 2 + j] = m.m[j * 2 + i];
      j ++;
    }
    i ++;
  }
  return y;
}