diff --git a/src/plugins/markdown-report/.gitignore b/src/plugins/markdown-report/.gitignore index 46c46f820766847e950d4c7024dce34c8f93e722..d3be7b0249a0805b8e0df1218976cfc3cffd4c91 100644 --- a/src/plugins/markdown-report/.gitignore +++ b/src/plugins/markdown-report/.gitignore @@ -9,3 +9,6 @@ top/ *~ /mdr_version.ml /Report_markdown.mli +/tests/ptests_config +/tests/*/result +/tests/*/result_* diff --git a/src/plugins/markdown-report/tests/eva/cwe126.c b/src/plugins/markdown-report/tests/eva/cwe126.c index ac01cb2b4ae432c7c30b3e8769910c5974a04f19..092f7b27f2105019614987e305524577d61cf350 100644 --- a/src/plugins/markdown-report/tests/eva/cwe126.c +++ b/src/plugins/markdown-report/tests/eva/cwe126.c @@ -1,3 +1,7 @@ +/* run.config + OPT: -mdr-remarks tests/eva/cwe126.remarks.md + */ + /* extracted from Juliet test suite v1.3 for C https://samate.nist.gov/SRD/view_testcase.php?tID=76270 */ diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md index 3d766a9a0d772510cbfe69f8d8d9725145d96026..7407b1429713869bae4d2c557ff06612baa42442 100644 --- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md +++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md @@ -7,6 +7,12 @@ date: 2019-10-25 \let\underscore\_ \renewcommand{\_}{\discretionary{\underscore}{}{\underscore}} +# Introduction {#intro} + +This is a test from the Juliet test suite showing an example of buffer +overflow (CWE126). The `good` functions should not trigger any alarm, while +the `bad` ones have indeed an error. + # Context of the analysis {#context} ## Input files {#c-input} @@ -20,9 +26,6 @@ that have been considered during the analysis are the following: ## Configuration {#options} -The options that have been used for this analysis are the following. - - ### EVA Domains {#domains} Only the base domain (`Cvalue`) has been used for the analysis @@ -57,10 +60,10 @@ Table: Warning reported by Frama-C | Location | Description | |:---------|:------------| -| tests/eva/cwe126.c:24 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) | +| tests/eva/cwe126.c:28 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) | -## Warning 0 (tests/eva/cwe126.c:24) {#warn-0} +## Warning 0 (tests/eva/cwe126.c:28) {#warn-0} ```log Message: out of bounds read. assert \valid_read(data + i); @@ -81,10 +84,10 @@ Table: Alarm emitted by the analysis | No | Kind | Emitter | Function | Location | |:---:|:----:|:-------:|:---------|:---------| -| [0](#alarm-0) | mem_access | Eva | CWE126_Buffer_Overread__malloc_char_loop_64b_badSink | tests/eva/cwe126.c:24 | +| [0](#alarm-0) | `mem_access` | `Eva` | `CWE126_Buffer_Overread__malloc_char_loop_64b_badSink` | tests/eva/cwe126.c:28 | -## Alarm 0 at tests/eva/cwe126.c:24 {#Alarm-0} +## Alarm 0 at tests/eva/cwe126.c:28 {#Alarm-0} The following ACSL assertion must hold to avoid an undefined behavior (mem_access) @@ -92,3 +95,7 @@ The following ACSL assertion must hold to avoid an undefined behavior (mem_acces assert mem_access: \valid_read(data + i); ``` + + +This alarm is real: Eva correctly identified the issue and did not report +any spurious alarm anywhere else. \ No newline at end of file diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle b/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle index 3dc206cbb24a5268e320fbd72063dad68b97138c..f07744fc4323039b628e134ac97025b35e15c362 100644 --- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle +++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle @@ -4,15 +4,15 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization -[eva] tests/eva/cwe126.c:72: allocating variable __malloc_goodG2B_l72 +[eva] tests/eva/cwe126.c:76: allocating variable __malloc_goodG2B_l76 [eva] using specification for function exit [eva] FRAMAC_SHARE/libc/string.h:118: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset -[eva] tests/eva/cwe126.c:58: starting to merge loop iterations -[eva] tests/eva/cwe126.c:36: - allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l36 -[eva] tests/eva/cwe126.c:22: starting to merge loop iterations -[eva:alarm] tests/eva/cwe126.c:24: Warning: +[eva] tests/eva/cwe126.c:62: starting to merge loop iterations +[eva] tests/eva/cwe126.c:40: + allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l40 +[eva] tests/eva/cwe126.c:26: starting to merge loop iterations +[eva:alarm] tests/eva/cwe126.c:28: Warning: out of bounds read. assert \valid_read(data + i); [eva] done for function main [eva] ====== VALUES COMPUTED ====== diff --git a/src/plugins/markdown-report/tests/eva/test_config b/src/plugins/markdown-report/tests/eva/test_config index ad6f78fce6e250ea58f66247b01f4aa600700ce4..02aa531013d392ec4dee76cd9c91015b86f4bb92 100644 --- a/src/plugins/markdown-report/tests/eva/test_config +++ b/src/plugins/markdown-report/tests/eva/test_config @@ -1,3 +1,2 @@ -CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-out @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.md +CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.@PTEST_NUMBER@.md LOG: @PTEST_NAME@.@PTEST_NUMBER@.md -OPT: