diff --git a/src/plugins/markdown-report/tests/sarif/cwe125.c b/src/plugins/markdown-report/tests/sarif/cwe125.c index 67fe3abe8dbd62ceeee320799d2241e24ea77d3f..4e3013719a1b91a9d99f904c7fc30fc044683df5 100644 --- a/src/plugins/markdown-report/tests/sarif/cwe125.c +++ b/src/plugins/markdown-report/tests/sarif/cwe125.c @@ -1,7 +1,7 @@ /* 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" diff --git a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.eva.log b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.eva.log new file mode 100644 index 0000000000000000000000000000000000000000..323a12ad49c4e847401a39ae747349b318011042 --- /dev/null +++ b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.eva.log @@ -0,0 +1,40 @@ +[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. + ---------------------------------------------------------------------------- diff --git a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.parse.log b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.parse.log new file mode 100644 index 0000000000000000000000000000000000000000..4d47a387d9d74a18432f685f935af07a67b325b9 --- /dev/null +++ b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.parse.log @@ -0,0 +1,3 @@ +[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?