[mdr] update test

src/plugins/markdown-report/.gitignore

@@ -9,3 +9,6 @@ top/
 *~
 /mdr_version.ml
 /Report_markdown.mli
+/tests/ptests_config
+/tests/*/result
+/tests/*/result_*

src/plugins/markdown-report/tests/eva/cwe126.c

+/* 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
 */

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

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 ======

src/plugins/markdown-report/tests/eva/test_config

-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: