Commit 58123e25 authored by Virgile Prevosto's avatar Virgile Prevosto Committed by Andre Maroneze
Browse files

[MdR] cleaner test output

parent 70bfa5dc
/* run.config
NOFRAMAC: use execnow for proper sequencing of executions
EXECNOW: @frama-c@ @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@_parse.sav
EXECNOW: @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_parse.sav -eva -save @PTEST_DIR@/result/@PTEST_NAME@_eva.sav
EXECNOW: LOG @PTEST_NAME@.parse.log @frama-c@ @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@_parse.sav > @PTEST_DIR@/result/@PTEST_NAME@.parse.log
EXECNOW: LOG @PTEST_NAME@.eva.log @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_parse.sav -eva -save @PTEST_DIR@/result/@PTEST_NAME@_eva.sav > @PTEST_DIR@/result/@PTEST_NAME@.eva.log
EXECNOW: LOG @PTEST_NAME@.sarif @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_eva.sav -then -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic
*/
#include "__fc_builtin.h"
......
[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.
----------------------------------------------------------------------------
[kernel] Parsing tests/sarif/cwe125.c (with preprocessing)
[kernel:typing:implicit-function-declaration] tests/sarif/cwe125.c:27: Warning:
Calling undeclared function printf. Old style K&R code?
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment