[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. ----------------------------------------------------------------------------