diff --git a/src/plugins/markdown-report/tests/md/cwe126.c b/src/plugins/markdown-report/tests/md/cwe126.c index c25b4aaa78d04b224c468e63122591835baa353c..b96948df6e500f229770267e52b4199900066e57 100644 --- a/src/plugins/markdown-report/tests/md/cwe126.c +++ b/src/plugins/markdown-report/tests/md/cwe126.c @@ -1,4 +1,5 @@ /* run.config + COMMENT: to uncomment with dune -> PLUGIN: @PTEST_PLUGIN@ markdown-report.eva-info OPT: -mdr-remarks %{dep:@PTEST_DIR@/@PTEST_NAME@.remarks.md} */ diff --git a/src/plugins/markdown-report/tests/md/oracle/cwe126.0.md b/src/plugins/markdown-report/tests/md/oracle/cwe126.0.md index bec42c33dbae166cc1c8012d038ecbacb61c977c..7cf06c232a619ad0ae15cd66cea3a3f08c8f3763 100644 --- a/src/plugins/markdown-report/tests/md/oracle/cwe126.0.md +++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.0.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). diff --git a/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle index 50108574f1711d4c7645fac9762815c185b5edfc..2bf983554f62d4a90cb998a5d513591d124d9345 100644 --- a/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle +++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle @@ -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 ======