diff --git a/src/plugins/markdown-report/Makefile.in b/src/plugins/markdown-report/Makefile.in index b599f8a4d684c741799f1795848e377b87f016d5..1adec8aa487ab7e020bccff40c7594fa694ffed3 100644 --- a/src/plugins/markdown-report/Makefile.in +++ b/src/plugins/markdown-report/Makefile.in @@ -39,7 +39,7 @@ PLUGIN_CMO:=\ PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE) PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure share/acsl.xml -PLUGIN_TESTS_DIRS:= eva sarif +PLUGIN_TESTS_DIRS:= md sarif include $(FRAMAC_SHARE)/Makefile.dynamic diff --git a/src/plugins/markdown-report/tests/eva/cwe126.c b/src/plugins/markdown-report/tests/md/cwe126.c similarity index 98% rename from src/plugins/markdown-report/tests/eva/cwe126.c rename to src/plugins/markdown-report/tests/md/cwe126.c index 092f7b27f2105019614987e305524577d61cf350..412e50978a77322fdd2d3f5ac8140ac9a33dafc7 100644 --- a/src/plugins/markdown-report/tests/eva/cwe126.c +++ b/src/plugins/markdown-report/tests/md/cwe126.c @@ -1,5 +1,5 @@ /* run.config - OPT: -mdr-remarks tests/eva/cwe126.remarks.md + OPT: -mdr-remarks @PTEST_DIR@/cwe126.remarks.md */ /* extracted from Juliet test suite v1.3 for C diff --git a/src/plugins/markdown-report/tests/eva/cwe126.remarks.md b/src/plugins/markdown-report/tests/md/cwe126.remarks.md similarity index 100% rename from src/plugins/markdown-report/tests/eva/cwe126.remarks.md rename to src/plugins/markdown-report/tests/md/cwe126.remarks.md diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md b/src/plugins/markdown-report/tests/md/oracle/cwe126.0.md similarity index 90% rename from src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md rename to src/plugins/markdown-report/tests/md/oracle/cwe126.0.md index 27c8a338e969cbc8e5b7d9a85d04cbac815be920..22a6d1e702051cc185f1bce1fb29ba87263f302d 100644 --- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md +++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.0.md @@ -20,7 +20,7 @@ the `bad` ones have indeed an error. The C source files (not including the headers `.h` files) that have been considered during the analysis are the following: -* `tests/eva/*.c` +* `tests/md/*.c` @@ -60,10 +60,10 @@ Table: Warning reported by Frama-C | Location | Description | |:---------|:------------| -| tests/eva/cwe126.c:28 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) | +| tests/md/cwe126.c:28 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) | -## Warning 0 (tests/eva/cwe126.c:28) {#warn-0} +## Warning 0 (tests/md/cwe126.c:28) {#warn-0} Message: @@ -87,10 +87,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:28 | +| [0](#alarm-0) | `mem_access` | `Eva` | `CWE126_Buffer_Overread__malloc_char_loop_64b_badSink` | tests/md/cwe126.c:28 | -## Alarm 0 at tests/eva/cwe126.c:28 {#Alarm-0} +## Alarm 0 at tests/md/cwe126.c:28 {#Alarm-0} The following ACSL assertion must hold to avoid invalid pointer dereferencing (undefined behavior). diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle similarity index 85% rename from src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle rename to src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle index f07744fc4323039b628e134ac97025b35e15c362..a303c721399c9ef094fce2029414b3205d549ab4 100644 --- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle +++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle @@ -1,18 +1,18 @@ -[kernel] Parsing tests/eva/cwe126.c (with preprocessing) +[kernel] Parsing tests/md/cwe126.c (with preprocessing) [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] tests/eva/cwe126.c:76: allocating variable __malloc_goodG2B_l76 +[eva] tests/md/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:62: starting to merge loop iterations -[eva] tests/eva/cwe126.c:40: +[eva] tests/md/cwe126.c:62: starting to merge loop iterations +[eva] tests/md/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: +[eva] tests/md/cwe126.c:26: starting to merge loop iterations +[eva:alarm] tests/md/cwe126.c:28: Warning: out of bounds read. assert \valid_read(data + i); [eva] done for function main [eva] ====== VALUES COMPUTED ====== @@ -54,4 +54,4 @@ Preconditions 8 valid 0 unknown 0 invalid 8 total 100% of the logical properties reached have been proven. ---------------------------------------------------------------------------- -[mdr] Report tests/eva/result/cwe126.0.md generated +[mdr] Report tests/md/result/cwe126.0.md generated diff --git a/src/plugins/markdown-report/tests/eva/test_config b/src/plugins/markdown-report/tests/md/test_config similarity index 100% rename from src/plugins/markdown-report/tests/eva/test_config rename to src/plugins/markdown-report/tests/md/test_config