From 32a822dd297bb6563dbbc1c002ca6294b702a93e Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 14 Oct 2020 23:06:22 +0200
Subject: [PATCH] [Markdown-report] add option -mdr-sarif-deterministic and
test
---
src/plugins/markdown-report/Makefile.in | 2 +-
src/plugins/markdown-report/mdr_params.ml | 7 +++++
src/plugins/markdown-report/mdr_params.mli | 3 ++
src/plugins/markdown-report/sarif_gen.ml | 19 +++++++++---
.../markdown-report/tests/sarif/libc.c | 8 +++--
.../tests/sarif/oracle/libc.0.res.oracle | 23 ++++++++++++++
.../tests/sarif/oracle/libc.1.res.oracle | 23 ++++++++++++++
.../tests/sarif/oracle/libc.res.oracle | 1 -
...{with-libc.sarif.clean => with-libc.sarif} | 31 ++++++++-----------
...ut-libc.sarif.clean => without-libc.sarif} | 31 ++++++++-----------
10 files changed, 102 insertions(+), 46 deletions(-)
create mode 100644 src/plugins/markdown-report/tests/sarif/oracle/libc.0.res.oracle
create mode 100644 src/plugins/markdown-report/tests/sarif/oracle/libc.1.res.oracle
delete mode 100644 src/plugins/markdown-report/tests/sarif/oracle/libc.res.oracle
rename src/plugins/markdown-report/tests/sarif/oracle/{with-libc.sarif.clean => with-libc.sarif} (99%)
rename src/plugins/markdown-report/tests/sarif/oracle/{without-libc.sarif.clean => without-libc.sarif} (68%)
diff --git a/src/plugins/markdown-report/Makefile.in b/src/plugins/markdown-report/Makefile.in
index 7b32d90509d..b599f8a4d68 100644
--- a/src/plugins/markdown-report/Makefile.in
+++ b/src/plugins/markdown-report/Makefile.in
@@ -39,7 +39,7 @@ PLUGIN_CMO:=\
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure share/acsl.xml
-PLUGIN_TESTS_DIRS:= eva
+PLUGIN_TESTS_DIRS:= eva sarif
include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/src/plugins/markdown-report/mdr_params.ml b/src/plugins/markdown-report/mdr_params.ml
index 6f1cbcdc05b..249abea7136 100644
--- a/src/plugins/markdown-report/mdr_params.ml
+++ b/src/plugins/markdown-report/mdr_params.ml
@@ -119,3 +119,10 @@ module PrintLibc = True(
let help =
"when set (default), reports include information about libc elements."
end)
+
+module SarifDeterministic = False(
+ struct
+ let option_name = "-mdr-sarif-deterministic"
+ let help = "omits non-deterministic data from SARIF reports, such as \
+ absolute file URIs and timestamps."
+ end)
diff --git a/src/plugins/markdown-report/mdr_params.mli b/src/plugins/markdown-report/mdr_params.mli
index b626fb52271..08b54d5c06f 100644
--- a/src/plugins/markdown-report/mdr_params.mli
+++ b/src/plugins/markdown-report/mdr_params.mli
@@ -48,3 +48,6 @@ module Stubs: Parameter_sig.String_list
(** Value of [-mdr-print-libc]. *)
module PrintLibc: Parameter_sig.Bool
+
+(** Value of [-mdr-sarif-deterministic]. *)
+module SarifDeterministic: Parameter_sig.Bool
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index a68a627085d..028ed32caaf 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -22,10 +22,14 @@
open Sarif
-let frama_c_sarif =
+let frama_c_sarif () =
let name = "frama-c" in
- let version = Fc_config.version_and_codename in
- let semanticVersion = Fc_config.version in
+ let version, semanticVersion =
+ if Mdr_params.SarifDeterministic.get () then
+ "omitted-for-deterministic-output", ""
+ else
+ Fc_config.version_and_codename, Fc_config.version
+ in
let fullName = name ^ "-" ^ version in
let downloadUri = "https://frama-c.com/download.html" in
let informationUri = "https://frama-c.com" in
@@ -209,7 +213,7 @@ let add_rule id desc l =
let make_taxonomies rules = Datatype.String.Map.fold add_rule rules []
let gen_run remarks =
- let tool = frama_c_sarif in
+ let tool = frama_c_sarif () in
let name = "frama-c" in
let invocations = [gen_invocation ()] in
let rules, results = gen_results remarks in
@@ -228,7 +232,12 @@ let gen_run remarks =
let uriBases = ("PWD", Sys.getcwd ()) :: Filepath.all_symbolic_dirs () in
let uriBasesJson =
List.fold_left (fun acc (name, dir) ->
- (name, `Assoc [("uri", `String ("file://" ^ dir ^ "/"))]) :: acc
+ let baseUri =
+ if Mdr_params.SarifDeterministic.get () then
+ "omitted-for-deterministic-output/"
+ else "file://" ^ dir ^ "/"
+ in
+ (name, `Assoc [("uri", `String baseUri)]) :: acc
) [] uriBases
in
let originalUriBaseIds =
diff --git a/src/plugins/markdown-report/tests/sarif/libc.c b/src/plugins/markdown-report/tests/sarif/libc.c
index b2458ae9458..2f7438beff3 100644
--- a/src/plugins/markdown-report/tests/sarif/libc.c
+++ b/src/plugins/markdown-report/tests/sarif/libc.c
@@ -1,7 +1,9 @@
/* run.config
- LOG: @PTEST_DIR@/oracle/with-libc.sarif.clean
- EXECNOW: @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -mdr-gen sarif -mdr-out @PTEST_DIR@/oracle/with-libc.sarif && sed -e "s:$FRAMAC_SHARE:REPLACED_FOR_PTESTS_FRAMAC_SHARE:g" -e "s:$FRAMAC_LIB:REPLACED_FOR_PTESTS_FRAMAC_LIB:g" -e "s:$FRAMAC_PLUGIN:REPLACED_FOR_PTESTS_FRAMAC_PLUGIN:g" -e "s:$PWD:REPLACED_FOR_PTESTS_PWD:g" @PTEST_DIR@/oracle/with-libc.sarif > @PTEST_DIR@/oracle/with-libc.sarif.clean && rm -f @PTEST_DIR@/oracle/with-libc.sarif
- EXECNOW: @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -mdr-gen sarif -mdr-out @PTEST_DIR@/oracle/without-libc.sarif -mdr-no-print-libc && sed -e "s:$FRAMAC_SHARE:REPLACED_FOR_PTESTS_FRAMAC_SHARE:g" -e "s:$FRAMAC_LIB:REPLACED_FOR_PTESTS_FRAMAC_LIB:g" -e "s:$FRAMAC_PLUGIN:REPLACED_FOR_PTESTS_FRAMAC_PLUGIN:g" -e "s:$PWD:REPLACED_FOR_PTESTS_PWD:g" @PTEST_DIR@/oracle/without-libc.sarif > @PTEST_DIR@/oracle/without-libc.sarif.clean && rm -f @PTEST_DIR@/oracle/without-libc.sarif
+ 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
+ LOG: with-libc.sarif
+ OPT: -mdr-out @PTEST_DIR@/result/with-libc.sarif
+ LOG: without-libc.sarif
+ OPT: -mdr-no-print-libc -mdr-out @PTEST_DIR@/result/without-libc.sarif
*/
#include <string.h>
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
new file mode 100644
index 00000000000..a64989bb4dd
--- /dev/null
+++ b/src/plugins/markdown-report/tests/sarif/oracle/libc.0.res.oracle
@@ -0,0 +1,23 @@
+[kernel] Parsing tests/sarif/libc.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] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 4 statements reached (out of 4): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ 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
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
new file mode 100644
index 00000000000..48818092e72
--- /dev/null
+++ b/src/plugins/markdown-report/tests/sarif/oracle/libc.1.res.oracle
@@ -0,0 +1,23 @@
+[kernel] Parsing tests/sarif/libc.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] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 4 statements reached (out of 4): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ 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
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/libc.res.oracle b/src/plugins/markdown-report/tests/sarif/oracle/libc.res.oracle
deleted file mode 100644
index 189063ded53..00000000000
--- a/src/plugins/markdown-report/tests/sarif/oracle/libc.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/sarif/libc.c (with preprocessing)
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif.clean b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
similarity index 99%
rename from src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif.clean
rename to src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
index 5ab08127ec0..5ea3f5bbff8 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif.clean
+++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
@@ -7,9 +7,8 @@
"tool": {
"driver": {
"name": "frama-c",
- "fullName": "frama-c-21.1+dev (Scandium)",
- "version": "21.1+dev (Scandium)",
- "semanticVersion": "21.1+dev",
+ "fullName": "frama-c-omitted-for-deterministic-output",
+ "version": "omitted-for-deterministic-output",
"downloadUri": "https://frama-c.com/download.html",
"informationUri": "https://frama-c.com"
}
@@ -17,27 +16,23 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -mdr-gen sarif -mdr-out tests/sarif/oracle/with-libc.sarif",
+ "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",
"arguments": [
"-check", "tests/sarif/libc.c", "-no-autoload-plugins",
"-load-module", "eva,from,scope,markdown_report", "-eva",
- "-mdr-gen", "sarif", "-mdr-out",
- "tests/sarif/oracle/with-libc.sarif"
+ "-eva-no-results", "-mdr-gen", "sarif",
+ "-mdr-sarif-deterministic", "-mdr-out",
+ "tests/sarif/result/with-libc.sarif"
],
"exitCode": 0,
"executionSuccessful": true
}
],
"originalUriBaseIds": {
- "FRAMAC_SHARE": { "uri": "file://REPLACED_FOR_PTESTS_FRAMAC_SHARE/" },
- "FRAMAC_LIB": { "uri": "file://REPLACED_FOR_PTESTS_FRAMAC_LIB/" },
- "FRAMAC_PLUGIN": {
- "uri": "file://REPLACED_FOR_PTESTS_FRAMAC_PLUGIN/"
- },
- "PWD": {
- "uri":
- "file://REPLACED_FOR_PTESTS_PWD/"
- }
+ "FRAMAC_SHARE": { "uri": "omitted-for-deterministic-output/" },
+ "FRAMAC_LIB": { "uri": "omitted-for-deterministic-output/" },
+ "FRAMAC_PLUGIN": { "uri": "omitted-for-deterministic-output/" },
+ "PWD": { "uri": "omitted-for-deterministic-output/" }
},
"artifacts": [
{
@@ -8686,12 +8681,12 @@
"physicalLocation": {
"artifactLocation": {
"uri":
- "REPLACED_FOR_PTESTS_PWD/tests/sarif/libc.c"
+ "/home/andr/git/frama-c-2/src/plugins/markdown-report/tests/sarif/libc.c"
},
"region": {
- "startLine": 11,
+ "startLine": 13,
"startColumn": 10,
- "endLine": 11,
+ "endLine": 13,
"endColumn": 19,
"byteLength": 9
}
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif.clean b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
similarity index 68%
rename from src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif.clean
rename to src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
index c874741c93b..d8cbdb4af85 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif.clean
+++ b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
@@ -7,9 +7,8 @@
"tool": {
"driver": {
"name": "frama-c",
- "fullName": "frama-c-21.1+dev (Scandium)",
- "version": "21.1+dev (Scandium)",
- "semanticVersion": "21.1+dev",
+ "fullName": "frama-c-omitted-for-deterministic-output",
+ "version": "omitted-for-deterministic-output",
"downloadUri": "https://frama-c.com/download.html",
"informationUri": "https://frama-c.com"
}
@@ -17,27 +16,23 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -mdr-gen sarif -mdr-out tests/sarif/oracle/without-libc.sarif -mdr-no-print-libc",
+ "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",
"arguments": [
"-check", "tests/sarif/libc.c", "-no-autoload-plugins",
"-load-module", "eva,from,scope,markdown_report", "-eva",
- "-mdr-gen", "sarif", "-mdr-out",
- "tests/sarif/oracle/without-libc.sarif", "-mdr-no-print-libc"
+ "-eva-no-results", "-mdr-gen", "sarif",
+ "-mdr-sarif-deterministic", "-mdr-no-print-libc", "-mdr-out",
+ "tests/sarif/result/without-libc.sarif"
],
"exitCode": 0,
"executionSuccessful": true
}
],
"originalUriBaseIds": {
- "FRAMAC_SHARE": { "uri": "file://REPLACED_FOR_PTESTS_FRAMAC_SHARE/" },
- "FRAMAC_LIB": { "uri": "file://REPLACED_FOR_PTESTS_FRAMAC_LIB/" },
- "FRAMAC_PLUGIN": {
- "uri": "file://REPLACED_FOR_PTESTS_FRAMAC_PLUGIN/"
- },
- "PWD": {
- "uri":
- "file://REPLACED_FOR_PTESTS_PWD/"
- }
+ "FRAMAC_SHARE": { "uri": "omitted-for-deterministic-output/" },
+ "FRAMAC_LIB": { "uri": "omitted-for-deterministic-output/" },
+ "FRAMAC_PLUGIN": { "uri": "omitted-for-deterministic-output/" },
+ "PWD": { "uri": "omitted-for-deterministic-output/" }
},
"artifacts": [
{
@@ -59,12 +54,12 @@
"physicalLocation": {
"artifactLocation": {
"uri":
- "REPLACED_FOR_PTESTS_PWD/tests/sarif/libc.c"
+ "/home/andr/git/frama-c-2/src/plugins/markdown-report/tests/sarif/libc.c"
},
"region": {
- "startLine": 11,
+ "startLine": 13,
"startColumn": 10,
- "endLine": 11,
+ "endLine": 13,
"endColumn": 19,
"byteLength": 9
}
--
GitLab