From adaf7cc27ac7c0567675ea7f06ce4ba0ac19db1d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 25 Oct 2019 13:08:35 +0200
Subject: [PATCH] [markdown] refactor example into tests
---
src/plugins/markdown-report/Makefile | 2 +-
.../{examples => tests/eva}/cwe126.c | 0
.../markdown-report/tests/eva/cwe126.md | 139 +++++++++++++++
.../eva/cwe126.remarks.md} | 161 ++----------------
.../tests/eva/oracle/cwe126.0.md | 95 +++++++++++
.../tests/eva/oracle/cwe126.res.oracle | 57 +++++++
.../tests/eva/result/cwe126.0.md | 95 +++++++++++
.../markdown-report/tests/eva/test_config | 3 +
.../markdown-report/tests/ptests_config | 7 +
9 files changed, 410 insertions(+), 149 deletions(-)
rename src/plugins/markdown-report/{examples => tests/eva}/cwe126.c (100%)
create mode 100644 src/plugins/markdown-report/tests/eva/cwe126.md
rename src/plugins/markdown-report/{examples/cwe126.remarks-sample.md => tests/eva/cwe126.remarks.md} (56%)
create mode 100644 src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
create mode 100644 src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
create mode 100644 src/plugins/markdown-report/tests/eva/result/cwe126.0.md
create mode 100644 src/plugins/markdown-report/tests/eva/test_config
create mode 100644 src/plugins/markdown-report/tests/ptests_config
diff --git a/src/plugins/markdown-report/Makefile b/src/plugins/markdown-report/Makefile
index a92ec35f6a8..b79cdd5d8d8 100644
--- a/src/plugins/markdown-report/Makefile
+++ b/src/plugins/markdown-report/Makefile
@@ -9,10 +9,10 @@ PLUGIN_GENERATED:=$(PLUGIN_DIR)/mdr_version.ml $(PLUGIN_DIR)/Report_markdown.mli
PLUGIN_CMO:=\
sarif mdr_version mdr_params parse_remarks \
eva_coverage md_gen sarif_gen mdr_register
-PLUGIN_NO_TEST:=true
PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson
PLUGIN_VERSION:=$(Report_markdown_VERSION)
PLUGIN_DISTRIB_EXTERNAL:=share/acsl.xml
+PLUGIN_TESTS_DIRS:= eva
include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/src/plugins/markdown-report/examples/cwe126.c b/src/plugins/markdown-report/tests/eva/cwe126.c
similarity index 100%
rename from src/plugins/markdown-report/examples/cwe126.c
rename to src/plugins/markdown-report/tests/eva/cwe126.c
diff --git a/src/plugins/markdown-report/tests/eva/cwe126.md b/src/plugins/markdown-report/tests/eva/cwe126.md
new file mode 100644
index 00000000000..5bc2b72680a
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/cwe126.md
@@ -0,0 +1,139 @@
+---
+title: Draft report
+author:
+date: 2019-10-25
+...
+
+\let\underscore\_
+\renewcommand{\_}{\discretionary{\underscore}{}{\underscore}}
+
+<!-- This file contains additional remarks that will be added to
+ automatically generated content by Frama-C's Markdown-report plugin. For
+ any section of the document, you can write pandoc markdown content
+ between the BEGIN and END comments. In addition, the plug-in will
+ consider any \<!-- INCLUDE file.md --\> comment (without backslashes) as
+ a directive to include the content of file.md in the corresponding
+ section. Please don't alter the structure of the document as it is used
+ by the plugin to associate content to the relevant section.
+-->
+
+# Introduction {#intro}
+
+<!-- You can add here some overall introduction to the analysis -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Context of the analysis {#context}
+
+## Input files {#c-input}
+
+<!-- You can add here some remarks about the set of files that is considered
+ by Frama-C
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+The C source files (not including the headers `.h` files)
+that have been considered during the analysis are the following:
+
+* `./*.c`
+
+
+
+## Configuration {#options}
+
+<!-- You can add here some remarks about the options used for the analysis
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+### EVA Domains {#domains}
+
+<!-- You can give more information about the choice of EVA domains -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+### Stubbed Functions {#stubs}
+
+<!-- You can add here general comments about the stubs that have been used
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+<!-- No stubs have been used -->
+
+# Coverage {#coverage}
+
+There are 6 function definitions that are not stubbed. They represent 50 statements, of which 50 are potentially reachable through EVA, resulting in a **statement coverage of 100.0%** with respect to the entire application.
+
+
+There were potentially 6 functions syntactically reachable from main.
+These functions contain 50 statements, of which 50 are potentially reachable according to EVA, resulting in a **statement coverage of 100.0%** with respect to the perimeter set by this entry point.
+
+
+<!-- You can comment on the coverage obtained by EVA -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Errors in the analyzer {#errors}
+
+<!-- you can comment on each individual error -->
+
+## Error 0 (Global) {#err-0}
+
+```log
+Message: Unable to open remarks file cwe126.remarks-sample.md (cwe126.remarks-sample.md: No such file or directory). No additional remarks will be included in the report.
+```
+
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Warnings {#warnings}
+
+<!-- you can comment on each individual error -->
+
+## Warning 0 (cwe126.c:24) {#warn-0}
+
+```log
+Message: out of bounds read. assert \valid_read(data + i);
+```
+
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Results of the analysis {#alarms}
+
+## Alarm 0 at cwe126.c:24 {#Alarm-0}
+
+```acsl
+assert mem_access: \valid_read(data + i);
+```
+
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Conclusion {#conclusion}
+
+<!-- You can put here some concluding remarks -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
\ No newline at end of file
diff --git a/src/plugins/markdown-report/examples/cwe126.remarks-sample.md b/src/plugins/markdown-report/tests/eva/cwe126.remarks.md
similarity index 56%
rename from src/plugins/markdown-report/examples/cwe126.remarks-sample.md
rename to src/plugins/markdown-report/tests/eva/cwe126.remarks.md
index b008643d0ee..9e40167cfed 100644
--- a/src/plugins/markdown-report/examples/cwe126.remarks-sample.md
+++ b/src/plugins/markdown-report/tests/eva/cwe126.remarks.md
@@ -1,7 +1,7 @@
---
title: Draft report
author:
-date: 2018-12-13
+date: 2019-10-25
...
\let\underscore\_
@@ -22,9 +22,11 @@ date: 2018-12-13
<!-- You can add here some overall introduction to the analysis -->
<!-- BEGIN_REMARK -->
+
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.
+
<!-- END_REMARK -->
# Context of the analysis {#context}
@@ -42,7 +44,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:
-* `cwe126.c`
+* `./*.c`
@@ -72,152 +74,15 @@ that have been considered during the analysis are the following:
<!-- END_REMARK -->
-<!-- You can add here general comments about the stubs that have been used
--->
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `char_equal_ignore_case` {#char_equal_ignore_case}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `memrchr` {#memrchr}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strcasecmp` {#strcasecmp}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strndup` {#strndup}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strdup` {#strdup}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strncat` {#strncat}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strcat` {#strcat}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strncpy` {#strncpy}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strcpy` {#strcpy}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strerror` {#strerror}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strstr` {#strstr}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strrchr` {#strrchr}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strchr` {#strchr}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strncmp` {#strncmp}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strcmp` {#strcmp}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strnlen` {#strnlen}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `strlen` {#strlen}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `memset` {#memset}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `memmove` {#memmove}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `memcpy` {#memcpy}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `memchr` {#memchr}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
-
-#### `memcmp` {#memcmp}
-
-<!-- BEGIN_REMARK -->
-
-<!-- END_REMARK -->
+<!-- No stubs have been used -->
# Coverage {#coverage}
-There are 6 function definitions that are not stubbed. They represent 50 statements, of which 43 are potentially reachable through EVA, resulting in a **statement coverage of 86.0%** with respect to the entire application.
+There are 6 function definitions that are not stubbed. They represent 50 statements, of which 50 are potentially reachable through EVA, resulting in a **statement coverage of 100.0%** with respect to the entire application.
There were potentially 6 functions syntactically reachable from main.
-These functions contain 50 statements, of which 43 are potentially reachable according to EVA, resulting in a **statement coverage of 86.0%** with respect to the perimeter set by this entry point.
+These functions contain 50 statements, of which 50 are potentially reachable according to EVA, resulting in a **statement coverage of 100.0%** with respect to the perimeter set by this entry point.
<!-- You can comment on the coverage obtained by EVA -->
@@ -232,10 +97,9 @@ These functions contain 50 statements, of which 43 are potentially reachable acc
## Warning 0 (cwe126.c:24) {#warn-0}
-message text is
-
-out of bounds read. assert \valid_read(data + i);
-
+```log
+Message: out of bounds read. assert \valid_read(data + i);
+```
<!-- BEGIN_REMARK -->
@@ -252,8 +116,10 @@ assert mem_access: \valid_read(data + i);
<!-- BEGIN_REMARK -->
+
This alarm is real: Eva correctly identified the issue and did not report
any spurious alarm anywhere else.
+
<!-- END_REMARK -->
# Conclusion {#conclusion}
@@ -262,5 +128,4 @@ any spurious alarm anywhere else.
<!-- BEGIN_REMARK -->
-<!-- END_REMARK -->
-
+<!-- END_REMARK -->
\ No newline at end of file
diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
new file mode 100644
index 00000000000..382c657cb9b
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
@@ -0,0 +1,95 @@
+---
+title: Frama-C Analysis Report
+author:
+date: 2019-10-25
+...
+
+\let\underscore\_
+\renewcommand{\_}{\discretionary{\underscore}{}{\underscore}}
+
+# Context of the analysis {#context}
+
+## Input files {#c-input}
+
+The C source files (not including the headers `.h` files)
+that have been considered during the analysis are the following:
+
+* `tests/eva/*.c`
+
+
+
+## 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
+
+
+### Stubbed Functions {#stubs}
+
+No stubs have been used for this analysis
+
+
+# Coverage {#coverage}
+
+There are 6 function definitions that are not stubbed. They represent 50 statements, of which 50 are potentially reachable through EVA, resulting in a **statement coverage of 100.0%** with respect to the entire application.
+
+
+There were potentially 6 functions syntactically reachable from main.
+These functions contain 50 statements, of which 50 are potentially reachable according to EVA, resulting in a **statement coverage of 100.0%** with respect to the perimeter set by this entry point.
+
+
+# Warnings {#warnings}
+
+The table below lists the warning that have been emitted by the analyzer.
+They might put additional assumptions on the relevance
+of the analysis results and must be reviewed carefully
+
+Note that this does not take into account emitted alarms:
+they are reported in [the next section](#alarms)
+
+
+
+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`) |
+
+
+## Warning 0 (tests/eva/cwe126.c:24) {#warn-0}
+
+```log
+Message: out of bounds read. assert \valid_read(data + i);
+```
+
+
+# Results of the analysis {#alarms}
+
+The table below lists the alarm that have been emitted during the analysis.
+Any execution starting from `main`
+in a context matching the one used for the analysis
+will be immune from any other undefined behavior.
+More information on each individual alarm is
+given in the remainder of this section
+
+
+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 |
+
+
+## Alarm 0 at tests/eva/cwe126.c:24 {#Alarm-0}
+
+The following ACSL assertion must hold to avoid an undefined behavior (mem_access)
+
+```acsl
+assert mem_access: \valid_read(data + i);
+```
+
diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle b/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
new file mode 100644
index 00000000000..3dc206cbb24
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
@@ -0,0 +1,57 @@
+[kernel] Parsing tests/eva/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:72: allocating variable __malloc_goodG2B_l72
+[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:
+ out of bounds read. assert \valid_read(data + i);
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states]
+ Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64b_badSink:
+ dataPtr ∈ {{ &data }}
+ data ∈ ESCAPINGADDR
+ data ∈ ESCAPINGADDR
+[eva:final-states]
+ Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64_bad:
+ __fc_heap_status ∈ [--..--]
+ data ∈ ESCAPINGADDR
+[eva:final-states]
+ Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64b_goodG2BSink:
+ dataPtr ∈ {{ &data }}
+ data ∈ ESCAPINGADDR
+ data ∈ ESCAPINGADDR
+[eva:final-states] Values at end of function goodG2B:
+ __fc_heap_status ∈ [--..--]
+ data ∈ ESCAPINGADDR
+[eva:final-states]
+ Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64_good:
+ __fc_heap_status ∈ [--..--]
+[eva:final-states] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
+ __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 6 functions analyzed (out of 6): 100% coverage.
+ In these functions, 54 statements reached (out of 54): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 invalid memory access
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ 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
diff --git a/src/plugins/markdown-report/tests/eva/result/cwe126.0.md b/src/plugins/markdown-report/tests/eva/result/cwe126.0.md
new file mode 100644
index 00000000000..382c657cb9b
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/result/cwe126.0.md
@@ -0,0 +1,95 @@
+---
+title: Frama-C Analysis Report
+author:
+date: 2019-10-25
+...
+
+\let\underscore\_
+\renewcommand{\_}{\discretionary{\underscore}{}{\underscore}}
+
+# Context of the analysis {#context}
+
+## Input files {#c-input}
+
+The C source files (not including the headers `.h` files)
+that have been considered during the analysis are the following:
+
+* `tests/eva/*.c`
+
+
+
+## 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
+
+
+### Stubbed Functions {#stubs}
+
+No stubs have been used for this analysis
+
+
+# Coverage {#coverage}
+
+There are 6 function definitions that are not stubbed. They represent 50 statements, of which 50 are potentially reachable through EVA, resulting in a **statement coverage of 100.0%** with respect to the entire application.
+
+
+There were potentially 6 functions syntactically reachable from main.
+These functions contain 50 statements, of which 50 are potentially reachable according to EVA, resulting in a **statement coverage of 100.0%** with respect to the perimeter set by this entry point.
+
+
+# Warnings {#warnings}
+
+The table below lists the warning that have been emitted by the analyzer.
+They might put additional assumptions on the relevance
+of the analysis results and must be reviewed carefully
+
+Note that this does not take into account emitted alarms:
+they are reported in [the next section](#alarms)
+
+
+
+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`) |
+
+
+## Warning 0 (tests/eva/cwe126.c:24) {#warn-0}
+
+```log
+Message: out of bounds read. assert \valid_read(data + i);
+```
+
+
+# Results of the analysis {#alarms}
+
+The table below lists the alarm that have been emitted during the analysis.
+Any execution starting from `main`
+in a context matching the one used for the analysis
+will be immune from any other undefined behavior.
+More information on each individual alarm is
+given in the remainder of this section
+
+
+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 |
+
+
+## Alarm 0 at tests/eva/cwe126.c:24 {#Alarm-0}
+
+The following ACSL assertion must hold to avoid an undefined behavior (mem_access)
+
+```acsl
+assert mem_access: \valid_read(data + i);
+```
+
diff --git a/src/plugins/markdown-report/tests/eva/test_config b/src/plugins/markdown-report/tests/eva/test_config
new file mode 100644
index 00000000000..ad6f78fce6e
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/test_config
@@ -0,0 +1,3 @@
+CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-out @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.md
+LOG: @PTEST_NAME@.@PTEST_NUMBER@.md
+OPT:
diff --git a/src/plugins/markdown-report/tests/ptests_config b/src/plugins/markdown-report/tests/ptests_config
new file mode 100644
index 00000000000..544cee504b6
--- /dev/null
+++ b/src/plugins/markdown-report/tests/ptests_config
@@ -0,0 +1,7 @@
+DEFAULT_SUITES= eva
+TOPLEVEL_PATH=/Users/correnson/Frama-C/trunk/bin/toplevel.opt
+FRAMAC_SHARE=/Users/correnson/Frama-C/trunk/share
+FRAMAC_LIB=/Users/correnson/Frama-C/trunk/lib/fc
+FRAMAC_PLUGIN=/Users/correnson/Frama-C/trunk/lib/plugins
+FRAMAC_PLUGIN_GUI=/Users/correnson/Frama-C/trunk/lib/plugins/gui
+OCAMLRUNPARAM=
--
GitLab