Skip to content
Snippets Groups Projects
Commit 2c514004 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[MdR] change test dir name

parent 37611ebd
No related branches found
No related tags found
No related merge requests found
...@@ -39,7 +39,7 @@ PLUGIN_CMO:=\ ...@@ -39,7 +39,7 @@ PLUGIN_CMO:=\
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE) PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure share/acsl.xml 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 include $(FRAMAC_SHARE)/Makefile.dynamic
......
/* run.config /* 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 /* extracted from Juliet test suite v1.3 for C
......
...@@ -20,7 +20,7 @@ the `bad` ones have indeed an error. ...@@ -20,7 +20,7 @@ the `bad` ones have indeed an error.
The C source files (not including the headers `.h` files) The C source files (not including the headers `.h` files)
that have been considered during the analysis are the following: 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 ...@@ -60,10 +60,10 @@ Table: Warning reported by Frama-C
| Location | Description | | 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: Message:
...@@ -87,10 +87,10 @@ Table: Alarm emitted by the analysis ...@@ -87,10 +87,10 @@ Table: Alarm emitted by the analysis
| No | Kind | Emitter | Function | Location | | 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 The following ACSL assertion must hold to avoid invalid pointer dereferencing
(undefined behavior). (undefined behavior).
......
[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] Analyzing a complete application starting at main
[eva] Computing initial state [eva] Computing initial state
[eva] Initial state computed [eva] Initial state computed
[eva:initial-state] Values of globals at initialization [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] using specification for function exit
[eva] FRAMAC_SHARE/libc/string.h:118: [eva] FRAMAC_SHARE/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva] tests/eva/cwe126.c:62: starting to merge loop iterations [eva] tests/md/cwe126.c:62: starting to merge loop iterations
[eva] tests/eva/cwe126.c:40: [eva] tests/md/cwe126.c:40:
allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l40 allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l40
[eva] tests/eva/cwe126.c:26: starting to merge loop iterations [eva] tests/md/cwe126.c:26: starting to merge loop iterations
[eva:alarm] tests/eva/cwe126.c:28: Warning: [eva:alarm] tests/md/cwe126.c:28: Warning:
out of bounds read. assert \valid_read(data + i); out of bounds read. assert \valid_read(data + i);
[eva] done for function main [eva] done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
...@@ -54,4 +54,4 @@ ...@@ -54,4 +54,4 @@
Preconditions 8 valid 0 unknown 0 invalid 8 total Preconditions 8 valid 0 unknown 0 invalid 8 total
100% of the logical properties reached have been proven. 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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment