Skip to content
Snippets Groups Projects
Commit 094200ec authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[Mdr] adds a comment line in a test

parent 4605970b
No related branches found
No related tags found
No related merge requests found
/* run.config
COMMENT: to uncomment with dune -> PLUGIN: @PTEST_PLUGIN@ markdown-report.eva-info
OPT: -mdr-remarks %{dep:@PTEST_DIR@/@PTEST_NAME@.remarks.md}
*/
......
......@@ -60,10 +60,10 @@ Table: Warning reported by Frama-C
| Location | Description |
|:---------|:------------|
| cwe126.c:28 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) |
| cwe126.c:29 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) |
## Warning 0 (cwe126.c:28) {#warn-0}
## Warning 0 (cwe126.c:29) {#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` | cwe126.c:28 |
| [0](#alarm-0) | `mem_access` | `Eva` | `CWE126_Buffer_Overread__malloc_char_loop_64b_badSink` | cwe126.c:29 |
## Alarm 0 at cwe126.c:28 {#Alarm-0}
## Alarm 0 at cwe126.c:29 {#Alarm-0}
The following ACSL assertion must hold to avoid invalid pointer dereferencing
(undefined behavior).
......
......@@ -4,15 +4,15 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva] cwe126.c:76: allocating variable __malloc_goodG2B_l76
[eva] cwe126.c:77: allocating variable __malloc_goodG2B_l77
[eva] using specification for function exit
[eva] FRAMAC_SHARE/libc/string.h:134:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva] cwe126.c:62: starting to merge loop iterations
[eva] cwe126.c:40:
allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l40
[eva] cwe126.c:26: starting to merge loop iterations
[eva:alarm] cwe126.c:28: Warning:
[eva] cwe126.c:63: starting to merge loop iterations
[eva] cwe126.c:41:
allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l41
[eva] cwe126.c:27: starting to merge loop iterations
[eva:alarm] cwe126.c:29: Warning:
out of bounds read. assert \valid_read(data + i);
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
......
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