From 7b87945e3b81a732f23315d0c74ec841ef9e7614 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 11 Mar 2021 14:11:10 +0100
Subject: [PATCH] [markdown-report] restore the test suite of the plug-in
---
src/plugins/markdown-report/tests/md/cwe126.c | 6 ----
.../tests/md/oracle/cwe126.0.md | 24 +++----------
.../tests/md/oracle/cwe126.res.oracle | 34 -------------------
.../markdown-report/tests/md/test_config | 2 +-
.../markdown-report/tests/ptests_config | 3 +-
.../markdown-report/tests/sarif/cwe125.c | 10 +++---
.../markdown-report/tests/sarif/libc.c | 8 ++---
.../tests/sarif/oracle/cwe125.res.oracle | 3 ++
.../tests/sarif/oracle/libc.0.res.oracle | 4 +--
.../tests/sarif/oracle/libc.1.res.oracle | 4 +--
.../tests/sarif/oracle/with-libc.sarif | 17 ++++------
.../tests/sarif/oracle/without-libc.sarif | 16 ++++-----
12 files changed, 35 insertions(+), 96 deletions(-)
create mode 100644 src/plugins/markdown-report/tests/sarif/oracle/cwe125.res.oracle
diff --git a/src/plugins/markdown-report/tests/md/cwe126.c b/src/plugins/markdown-report/tests/md/cwe126.c
index 41e14b8fb93..7f0a46663dc 100644
--- a/src/plugins/markdown-report/tests/md/cwe126.c
+++ b/src/plugins/markdown-report/tests/md/cwe126.c
@@ -1,11 +1,5 @@
/* run.config
-<<<<<<< HEAD:src/plugins/markdown-report/tests/eva/cwe126.c
STDOPT: +"-mdr-remarks %{dep:@PTEST_NAME@.remarks.md}"
-||||||| ac7807782d:src/plugins/markdown-report/tests/eva/cwe126.c
- OPT: -mdr-remarks tests/eva/cwe126.remarks.md
-=======
- OPT: -mdr-remarks @PTEST_DIR@/cwe126.remarks.md
->>>>>>> origin/master:src/plugins/markdown-report/tests/md/cwe126.c
*/
/* extracted from Juliet test suite v1.3 for C
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 4fddd3e2ba0..e12065d755d 100644
--- a/src/plugins/markdown-report/tests/md/oracle/cwe126.0.md
+++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.0.md
@@ -20,31 +20,17 @@ 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:
-* `tests/md/*.c`
+* `./*.c`
## Configuration {#options}
-### 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.
@@ -60,10 +46,10 @@ Table: Warning reported by Frama-C
| Location | Description |
|:---------|:------------|
-| tests/md/cwe126.c:28 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) |
+| cwe126.c:28 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) |
-## Warning 0 (tests/md/cwe126.c:28) {#warn-0}
+## Warning 0 (cwe126.c:28) {#warn-0}
Message:
@@ -87,10 +73,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/md/cwe126.c:28 |
+| [0](#alarm-0) | `mem_access` | `Eva` | `CWE126_Buffer_Overread__malloc_char_loop_64b_badSink` | cwe126.c:28 |
-## Alarm 0 at tests/md/cwe126.c:28 {#Alarm-0}
+## Alarm 0 at cwe126.c:28 {#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 f802f141c78..ada3b892d20 100644
--- a/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
+++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
@@ -1,46 +1,18 @@
-<<<<<<< HEAD:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
[kernel] Parsing cwe126.c (with preprocessing)
-||||||| ac7807782d:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
-[kernel] Parsing tests/eva/cwe126.c (with preprocessing)
-=======
-[kernel] Parsing tests/md/cwe126.c (with preprocessing)
->>>>>>> origin/master:src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-<<<<<<< HEAD:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
[eva] cwe126.c:76: allocating variable __malloc_goodG2B_l76
-||||||| ac7807782d:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
-[eva] tests/eva/cwe126.c:76: allocating variable __malloc_goodG2B_l76
-=======
-[eva] tests/md/cwe126.c:76: allocating variable __malloc_goodG2B_l76
->>>>>>> origin/master:src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
[eva] using specification for function exit
[eva] FRAMAC_SHARE/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
-<<<<<<< HEAD:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
[eva] cwe126.c:62: starting to merge loop iterations
[eva] cwe126.c:40:
-||||||| ac7807782d:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
-[eva] tests/eva/cwe126.c:62: starting to merge loop iterations
-[eva] tests/eva/cwe126.c:40:
-=======
-[eva] tests/md/cwe126.c:62: starting to merge loop iterations
-[eva] tests/md/cwe126.c:40:
->>>>>>> origin/master:src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l40
-<<<<<<< HEAD:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
[eva] cwe126.c:26: starting to merge loop iterations
[eva:alarm] cwe126.c:28: Warning:
-||||||| ac7807782d:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
-[eva] tests/eva/cwe126.c:26: starting to merge loop iterations
-[eva:alarm] tests/eva/cwe126.c:28: Warning:
-=======
-[eva] tests/md/cwe126.c:26: starting to merge loop iterations
-[eva:alarm] tests/md/cwe126.c:28: Warning:
->>>>>>> origin/master:src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
out of bounds read. assert \valid_read(data + i);
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -82,10 +54,4 @@
Preconditions 8 valid 0 unknown 0 invalid 8 total
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
-<<<<<<< HEAD:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
[mdr] Report cwe126.0.md generated
-||||||| ac7807782d:src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
-[mdr] Report tests/eva/result/cwe126.0.md generated
-=======
-[mdr] Report tests/md/result/cwe126.0.md generated
->>>>>>> origin/master:src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
diff --git a/src/plugins/markdown-report/tests/md/test_config b/src/plugins/markdown-report/tests/md/test_config
index c7be0c1d592..0f0e659ccc5 100644
--- a/src/plugins/markdown-report/tests/md/test_config
+++ b/src/plugins/markdown-report/tests/md/test_config
@@ -1,3 +1,3 @@
PLUGIN: markdown-report eva inout
-OPT: -eva -then -mdr-gen md -mdr-date="now" -mdr-out @PTEST_NAME@.@PTEST_NUMBER@.md
LOG: @PTEST_NAME@.@PTEST_NUMBER@.md
+OPT: -eva -then -mdr-gen md -mdr-date="now" -mdr-out @PTEST_NAME@.@PTEST_NUMBER@.md
diff --git a/src/plugins/markdown-report/tests/ptests_config b/src/plugins/markdown-report/tests/ptests_config
index b7fbf751c51..0cc5fff411d 100644
--- a/src/plugins/markdown-report/tests/ptests_config
+++ b/src/plugins/markdown-report/tests/ptests_config
@@ -1,2 +1 @@
-IGNORE:= DEFAULT_SUITES= md
-IGNORE:= DEFAULT_SUITES= sarif
+DEFAULT_SUITES= md sarif
diff --git a/src/plugins/markdown-report/tests/sarif/cwe125.c b/src/plugins/markdown-report/tests/sarif/cwe125.c
index 4e3013719a1..c47f343b3bd 100644
--- a/src/plugins/markdown-report/tests/sarif/cwe125.c
+++ b/src/plugins/markdown-report/tests/sarif/cwe125.c
@@ -1,8 +1,8 @@
-/* run.config
-NOFRAMAC: use execnow for proper sequencing of executions
-EXECNOW: LOG @PTEST_NAME@.parse.log @frama-c@ @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@_parse.sav > @PTEST_DIR@/result/@PTEST_NAME@.parse.log
-EXECNOW: LOG @PTEST_NAME@.eva.log @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_parse.sav -eva -save @PTEST_DIR@/result/@PTEST_NAME@_eva.sav > @PTEST_DIR@/result/@PTEST_NAME@.eva.log
-EXECNOW: LOG @PTEST_NAME@.sarif @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_eva.sav -then -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic
+/* run.config NOFRAMAC: use execnow for proper sequencing of executions
+PLUGIN: markdown-report eva inout
+EXECNOW: LOG @PTEST_NAME@.parse.log LOG @PTEST_NAME@.parse.err LOG @PTEST_NAME@_parse.sav @frama-c@ -save @PTEST_NAME@_parse.sav > @PTEST_NAME@.parse.log 2> @PTEST_NAME@.parse.err
+EXECNOW: LOG @PTEST_NAME@.eva.log LOG @PTEST_NAME@.eva.err LOG @PTEST_NAME@_eva.sav @frama-c-cmd@ -load %{dep:@PTEST_NAME@_parse.sav} -eva -save @PTEST_NAME@_eva.sav > @PTEST_NAME@.eva.log 2> @PTEST_NAME@.eva.err
+EXECNOW: LOG @PTEST_NAME@.sarif.log LOG @PTEST_NAME@.sarif.err LOG @PTEST_NAME@.sarif @frama-c-cmd@ -load %{dep:@PTEST_NAME@_eva.sav} -then -mdr-out @PTEST_NAME@.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic > @PTEST_NAME@.sarif.log 2> @PTEST_NAME@.sarif.err
*/
#include "__fc_builtin.h"
diff --git a/src/plugins/markdown-report/tests/sarif/libc.c b/src/plugins/markdown-report/tests/sarif/libc.c
index 2f7438beff3..c3b96454fa0 100644
--- a/src/plugins/markdown-report/tests/sarif/libc.c
+++ b/src/plugins/markdown-report/tests/sarif/libc.c
@@ -1,11 +1,11 @@
/* run.config
- CMD: @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
+ PLUGIN: eva,from,scope,markdown-report
+ MACRO: TEST_OPTION -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
LOG: with-libc.sarif
- OPT: -mdr-out @PTEST_DIR@/result/with-libc.sarif
+ OPT: @TEST_OPTION@ -mdr-out with-libc.sarif
LOG: without-libc.sarif
- OPT: -mdr-no-print-libc -mdr-out @PTEST_DIR@/result/without-libc.sarif
+ OPT: @TEST_OPTION@ -mdr-no-print-libc -mdr-out without-libc.sarif
*/
-
#include <string.h>
int main() {
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.res.oracle b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.res.oracle
new file mode 100644
index 00000000000..0ef7666c977
--- /dev/null
+++ b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing cwe125.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] cwe125.c:27: Warning:
+ Calling undeclared function printf. Old style K&R code?
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/libc.0.res.oracle b/src/plugins/markdown-report/tests/sarif/oracle/libc.0.res.oracle
index a64989bb4dd..34bcdb93fb4 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/libc.0.res.oracle
+++ b/src/plugins/markdown-report/tests/sarif/oracle/libc.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/sarif/libc.c (with preprocessing)
+[kernel] Parsing libc.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -20,4 +20,4 @@
Preconditions 1 valid 0 unknown 0 invalid 1 total
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
-[mdr] Report tests/sarif/result/with-libc.sarif generated
+[mdr] Report with-libc.sarif generated
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/libc.1.res.oracle b/src/plugins/markdown-report/tests/sarif/oracle/libc.1.res.oracle
index 48818092e72..8888de2a968 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/libc.1.res.oracle
+++ b/src/plugins/markdown-report/tests/sarif/oracle/libc.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/sarif/libc.c (with preprocessing)
+[kernel] Parsing libc.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -20,4 +20,4 @@
Preconditions 1 valid 0 unknown 0 invalid 1 total
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
-[mdr] Report tests/sarif/result/without-libc.sarif generated
+[mdr] Report without-libc.sarif generated
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
index fa8798f3f64..2224da9ff88 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
@@ -16,13 +16,12 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-out tests/sarif/result/with-libc.sarif",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-plugin=eva,from,scope,markdown-report libc.c -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-out with-libc.sarif",
"arguments": [
- "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
- "-load-module", "eva,from,scope,markdown_report", "-eva",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-plugin=eva,from,scope,markdown-report", "libc.c", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
- "-mdr-sarif-deterministic", "-mdr-out",
- "tests/sarif/result/with-libc.sarif"
+ "-mdr-sarif-deterministic", "-mdr-out", "with-libc.sarif"
],
"exitCode": 0,
"executionSuccessful": true
@@ -32,7 +31,6 @@
"FRAMAC_SHARE": {
"uri": "file:///omitted-for-deterministic-output/"
},
- "FRAMAC_LIB": { "uri": "file:///omitted-for-deterministic-output/" },
"FRAMAC_PLUGIN": {
"uri": "file:///omitted-for-deterministic-output/"
},
@@ -40,7 +38,7 @@
},
"artifacts": [
{
- "location": { "uri": "tests/sarif/libc.c", "uriBaseId": "PWD" },
+ "location": { "uri": "libc.c", "uriBaseId": "PWD" },
"roles": [ "analysisTarget" ],
"mimeType": "text/x-csrc"
}
@@ -8683,10 +8681,7 @@
"locations": [
{
"physicalLocation": {
- "artifactLocation": {
- "uri": "tests/sarif/libc.c",
- "uriBaseId": "PWD"
- },
+ "artifactLocation": { "uri": "libc.c", "uriBaseId": "PWD" },
"region": {
"startLine": 13,
"startColumn": 10,
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
index b22b1bf8f42..461ef8f3606 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
@@ -16,13 +16,13 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-no-print-libc -mdr-out tests/sarif/result/without-libc.sarif",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-plugin=eva,from,scope,markdown-report libc.c -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-no-print-libc -mdr-out without-libc.sarif",
"arguments": [
- "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
- "-load-module", "eva,from,scope,markdown_report", "-eva",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-plugin=eva,from,scope,markdown-report", "libc.c", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
"-mdr-sarif-deterministic", "-mdr-no-print-libc", "-mdr-out",
- "tests/sarif/result/without-libc.sarif"
+ "without-libc.sarif"
],
"exitCode": 0,
"executionSuccessful": true
@@ -32,7 +32,6 @@
"FRAMAC_SHARE": {
"uri": "file:///omitted-for-deterministic-output/"
},
- "FRAMAC_LIB": { "uri": "file:///omitted-for-deterministic-output/" },
"FRAMAC_PLUGIN": {
"uri": "file:///omitted-for-deterministic-output/"
},
@@ -40,7 +39,7 @@
},
"artifacts": [
{
- "location": { "uri": "tests/sarif/libc.c", "uriBaseId": "PWD" },
+ "location": { "uri": "libc.c", "uriBaseId": "PWD" },
"roles": [ "analysisTarget" ],
"mimeType": "text/x-csrc"
}
@@ -56,10 +55,7 @@
"locations": [
{
"physicalLocation": {
- "artifactLocation": {
- "uri": "tests/sarif/libc.c",
- "uriBaseId": "PWD"
- },
+ "artifactLocation": { "uri": "libc.c", "uriBaseId": "PWD" },
"region": {
"startLine": 13,
"startColumn": 10,
--
GitLab