[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] using specification for function Frama_C_interval
[eva:alarm] tests/sarif/cwe125.c:21: Warning: 
  out of bounds read. assert \valid_read(array + index);
[eva:alarm] tests/sarif/cwe125.c:27: Warning: 
  out of bounds read. assert \valid_read(array + index);
[eva] done for function main
[eva] tests/sarif/cwe125.c:27: 
  assertion 'Eva,mem_access' got final status invalid.
[kernel:annot:missing-spec] tests/sarif/cwe125.c:27: Warning: 
  Neither code nor specification for function printf, generating default assigns from the prototype
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function getValueFromArray:
  value ∈ {0}
[eva:final-states] Values at end of function main:
  Frama_C_entropy_source ∈ [--..--]
  arr[0..9] ∈ {0}
  test ∈ [0..9]
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  2 functions analyzed (out of 2): 100% coverage.
  In these functions, 8 statements reached (out of 9): 88% coverage.
  ----------------------------------------------------------------------------
  Some errors and warnings have been raised during the analysis:
    by the Eva analyzer:      0 errors    0 warnings
    by the Frama-C kernel:    0 errors    2 warnings
  ----------------------------------------------------------------------------
  2 alarms generated by the analysis:
       2 invalid memory accesses
  1 of them is a sure alarm (invalid status).
  ----------------------------------------------------------------------------
  Evaluation of the logical properties reached by the analysis:
    Assertions        0 valid     0 unknown     0 invalid      0 total
    Preconditions     1 valid     0 unknown     0 invalid      1 total
  100% of the logical properties reached have been proven.
  ----------------------------------------------------------------------------