[eva] Analyzing a complete application starting at main
[eva:initial-state] Values of globals at initialization
  aorai_CurOperation ∈ {op_main}
  aorai_CurOpStatus ∈ {aorai_Called}
  aorai_CurStates ∈ {init}
[aorai] saveload.i:14: accept
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f_post_func:
  aorai_CurOperation ∈ {op_f}
  aorai_CurOpStatus ∈ {aorai_Terminated}
  aorai_CurStates ∈ {accept}
[eva:final-states] Values at end of function f_pre_func:
  aorai_CurOperation ∈ {op_f}
  aorai_CurOpStatus ∈ {aorai_Called}
  aorai_CurStates ∈ {accept}
[eva:final-states] Values at end of function f:
  aorai_CurOperation ∈ {op_f}
  aorai_CurOpStatus ∈ {aorai_Terminated}
  aorai_CurStates ∈ {accept}
[eva:final-states] Values at end of function main_post_func:
  aorai_CurOperation ∈ {op_main}
  aorai_CurOpStatus ∈ {aorai_Terminated}
  aorai_CurStates ∈ {accept}
[eva:final-states] Values at end of function main_pre_func:
  aorai_CurOperation ∈ {op_main}
  aorai_CurOpStatus ∈ {aorai_Called}
  aorai_CurStates ∈ {accept}
[eva:final-states] Values at end of function main:
  __retres ∈ {0}
  aorai_CurOperation ∈ {op_main}
  aorai_CurOpStatus ∈ {aorai_Terminated}
  aorai_CurStates ∈ {accept}
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  6 functions analyzed (out of 6): 100% coverage.
  In these functions, 31 statements reached (out of 35): 89% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  0 alarms generated by the analysis.
  ----------------------------------------------------------------------------
  Evaluation of the logical properties reached by the analysis:
    Assertions        0 valid     0 unknown     0 invalid      0 total
    Preconditions     5 valid     0 unknown     0 invalid      5 total
  100% of the logical properties reached have been proven.
  ----------------------------------------------------------------------------
