Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
32a822dd
Commit
32a822dd
authored
Oct 14, 2020
by
Andre Maroneze
💬
Committed by
Virgile Prevosto
Oct 19, 2020
Browse files
[Markdown-report] add option -mdr-sarif-deterministic and test
parent
ca15ad69
Changes
10
Hide whitespace changes
Inline
Side-by-side
src/plugins/markdown-report/Makefile.in
View file @
32a822dd
...
...
@@ -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
...
...
src/plugins/markdown-report/mdr_params.ml
View file @
32a822dd
...
...
@@ -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
)
src/plugins/markdown-report/mdr_params.mli
View file @
32a822dd
...
...
@@ -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
src/plugins/markdown-report/sarif_gen.ml
View file @
32a822dd
...
...
@@ -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
=
...
...
src/plugins/markdown-report/tests/sarif/libc.c
View file @
32a822dd
/* 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>
...
...
src/plugins/markdown-report/tests/sarif/oracle/libc.0.res.oracle
0 → 100644
View file @
32a822dd
[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
src/plugins/markdown-report/tests/sarif/oracle/libc.1.res.oracle
0 → 100644
View file @
32a822dd
[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
src/plugins/markdown-report/tests/sarif/oracle/libc.res.oracle
deleted
100644 → 0
View file @
ca15ad69
[kernel] Parsing tests/sarif/libc.c (with preprocessing)
src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
.clean
→
src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
View file @
32a822dd
...
...
@@ -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": 1
1
,
"startLine": 1
3
,
"startColumn": 10,
"endLine": 1
1
,
"endLine": 1
3
,
"endColumn": 19,
"byteLength": 9
}
...
...
src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
.clean
→
src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
View file @
32a822dd
...
...
@@ -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": 1
1
,
"startLine": 1
3
,
"startColumn": 10,
"endLine": 1
1
,
"endLine": 1
3
,
"endColumn": 19,
"byteLength": 9
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment