extern_init.1.res.oracle

[kernel] Parsing tests/syntax/extern_init.i (no preprocessing)
[kernel] Parsing tests/syntax/extern_init_2.i (no preprocessing)
[kernel:typing:no-proto] tests/syntax/extern_init_2.i:10: Warning: 
  Calling function f that is declared without prototype.
  Its formals will be inferred from actual arguments
[kernel:typing:no-proto] tests/syntax/extern_init_2.i:11: Warning: 
  Calling function g that is declared without prototype.
  Its formals will be inferred from actual arguments
[kernel] Parsing tests/syntax/extern_init_1.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  a[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {4}
   [4] ∈ {5}
[eva] computing for function f <- main.
  Called from tests/syntax/extern_init_2.i:10.
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
  Called from tests/syntax/extern_init_2.i:11.
[eva] using specification for function g
[eva] Done for function g
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
  a[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {12}
   [3] ∈ {4}
   [4] ∈ {5}
[eva:final-states] Values at end of function main:
  a[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {12}
   [3] ∈ [--..--]
   [4] ∈ {5}
  __retres ∈ {2}