diff --git a/src/plugins/markdown-report/Makefile.in b/src/plugins/markdown-report/Makefile.in
index b599f8a4d684c741799f1795848e377b87f016d5..1adec8aa487ab7e020bccff40c7594fa694ffed3 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 sarif
+PLUGIN_TESTS_DIRS:= md sarif
include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 82d6faa27133c3ed628271fb76b155a2426e1246..fce40cc7d22fe0d29b370a9f02f018cc3406be8f 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -47,24 +47,34 @@ let get_remark remarks label =
| None -> []
| Some l -> l
-let command_line () = Array.to_list Sys.argv
-
+(* keep track of command line arguments for all invocations of Frama-C during
+ a save/load sequence. Note that the list is in reverse order
+ (newest invocation first).
+*)
module Analysis_cmdline =
- State_builder.Ref(Datatype.List(Datatype.String))
+ State_builder.List_ref(Datatype.List(Datatype.String))
(struct
let name = "Sarif_gen.Analysis_cmdline"
let dependencies = []
- let default = command_line
end)
+let command_line () = Array.to_list Sys.argv
+
+let update_cmdline () = Analysis_cmdline.add (command_line())
+
+let () = Cmdline.run_after_loading_stage update_cmdline
+
let gen_invocation () =
- let cl = Analysis_cmdline.get () in
- (* The first argument is _always_ the binary name, but to avoid printing it
- as an absolute path to binlevel.opt, we replace it with 'frama-c' *)
- let cl = "frama-c" :: List.tl cl in
- let commandLine = String.concat " " cl in
- let arguments = List.tl cl in
- Invocation.create ~commandLine ~arguments ()
+ let cls = Analysis_cmdline.get () in
+ let gen_one cl =
+ (* The first argument is _always_ the binary name, but to avoid printing it
+ as an absolute path to binlevel.opt, we replace it with 'frama-c' *)
+ let cl = "frama-c" :: List.tl cl in
+ let commandLine = String.concat " " cl in
+ let arguments = List.tl cl in
+ Invocation.create ~commandLine ~arguments ()
+ in
+ List.rev_map gen_one cls
let gen_remark alarm =
let open Markdown in
@@ -215,7 +225,7 @@ let make_taxonomies rules = Datatype.String.Map.fold add_rule rules []
let gen_run remarks =
let tool = frama_c_sarif () in
let name = "frama-c" in
- let invocations = [gen_invocation ()] in
+ let invocations = gen_invocation () in
let rules, results = gen_results remarks in
let user_annot_results = gen_statuses () in
let rules =
diff --git a/src/plugins/markdown-report/tests/eva/cwe126.c b/src/plugins/markdown-report/tests/md/cwe126.c
similarity index 98%
rename from src/plugins/markdown-report/tests/eva/cwe126.c
rename to src/plugins/markdown-report/tests/md/cwe126.c
index 092f7b27f2105019614987e305524577d61cf350..412e50978a77322fdd2d3f5ac8140ac9a33dafc7 100644
--- a/src/plugins/markdown-report/tests/eva/cwe126.c
+++ b/src/plugins/markdown-report/tests/md/cwe126.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -mdr-remarks tests/eva/cwe126.remarks.md
+ OPT: -mdr-remarks @PTEST_DIR@/cwe126.remarks.md
*/
/* extracted from Juliet test suite v1.3 for C
diff --git a/src/plugins/markdown-report/tests/eva/cwe126.remarks.md b/src/plugins/markdown-report/tests/md/cwe126.remarks.md
similarity index 100%
rename from src/plugins/markdown-report/tests/eva/cwe126.remarks.md
rename to src/plugins/markdown-report/tests/md/cwe126.remarks.md
diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md b/src/plugins/markdown-report/tests/md/oracle/cwe126.0.md
similarity index 90%
rename from src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
rename to src/plugins/markdown-report/tests/md/oracle/cwe126.0.md
index 27c8a338e969cbc8e5b7d9a85d04cbac815be920..22a6d1e702051cc185f1bce1fb29ba87263f302d 100644
--- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
+++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.0.md
@@ -20,7 +20,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:
-* `tests/eva/*.c`
+* `tests/md/*.c`
@@ -60,10 +60,10 @@ Table: Warning reported by Frama-C
| Location | Description |
|:---------|:------------|
-| tests/eva/cwe126.c:28 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) |
+| tests/md/cwe126.c:28 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) |
-## Warning 0 (tests/eva/cwe126.c:28) {#warn-0}
+## Warning 0 (tests/md/cwe126.c:28) {#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` | tests/eva/cwe126.c:28 |
+| [0](#alarm-0) | `mem_access` | `Eva` | `CWE126_Buffer_Overread__malloc_char_loop_64b_badSink` | tests/md/cwe126.c:28 |
-## Alarm 0 at tests/eva/cwe126.c:28 {#Alarm-0}
+## Alarm 0 at tests/md/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/eva/oracle/cwe126.res.oracle b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
similarity index 85%
rename from src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
rename to src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
index f07744fc4323039b628e134ac97025b35e15c362..a303c721399c9ef094fce2029414b3205d549ab4 100644
--- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
+++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
@@ -1,18 +1,18 @@
-[kernel] Parsing tests/eva/cwe126.c (with preprocessing)
+[kernel] Parsing tests/md/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:76: allocating variable __malloc_goodG2B_l76
+[eva] tests/md/cwe126.c:76: allocating variable __malloc_goodG2B_l76
[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: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:
allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l40
-[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:
out of bounds read. assert \valid_read(data + i);
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -54,4 +54,4 @@
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
+[mdr] Report tests/md/result/cwe126.0.md generated
diff --git a/src/plugins/markdown-report/tests/eva/test_config b/src/plugins/markdown-report/tests/md/test_config
similarity index 100%
rename from src/plugins/markdown-report/tests/eva/test_config
rename to src/plugins/markdown-report/tests/md/test_config
diff --git a/src/plugins/markdown-report/tests/sarif/cwe125.c b/src/plugins/markdown-report/tests/sarif/cwe125.c
new file mode 100644
index 0000000000000000000000000000000000000000..67fe3abe8dbd62ceeee320799d2241e24ea77d3f
--- /dev/null
+++ b/src/plugins/markdown-report/tests/sarif/cwe125.c
@@ -0,0 +1,38 @@
+/* run.config
+NOFRAMAC: use execnow for proper sequencing of executions
+EXECNOW: @frama-c@ @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@_parse.sav
+EXECNOW: @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_parse.sav -eva -save @PTEST_DIR@/result/@PTEST_NAME@_eva.sav
+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
+*/
+#include "__fc_builtin.h"
+
+#define LENGTH 10
+
+int getValueFromArray(int *array, int len, int index) {
+
+int value;
+
+// check that the array index is less than the maximum
+
+// length of the array
+if (index < len) {
+
+// get the value at the specified index of the array
+value = array[index];
+}
+// if array index is invalid then output error message
+
+// and return value indicating error
+else {
+printf("Value is: %d\n", array[index]);
+value = -1;
+}
+
+return value;
+}
+
+int main() {
+ int arr[LENGTH] = { 0 };
+ int test = Frama_C_interval(-LENGTH,LENGTH);
+ return getValueFromArray(arr,LENGTH,test);
+}
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
new file mode 100644
index 0000000000000000000000000000000000000000..3c9e422059821ea9c926da5d88f029e0ddf8a331
--- /dev/null
+++ b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
@@ -0,0 +1,269 @@
+{
+ "$schema":
+ "https://github.com/oasis-tcs/sarif-spec/blob/master/Documents/CommitteeSpecificationDrafts/v2.1.0-CSD.1/sarif-schema-2.1.0.json",
+ "version": "2.1.0",
+ "runs": [
+ {
+ "tool": {
+ "driver": {
+ "name": "frama-c",
+ "fullName": "frama-c-0+omitted-for-deterministic-output",
+ "version": "0+omitted-for-deterministic-output",
+ "downloadUri": "https://frama-c.com/download.html",
+ "informationUri": "https://frama-c.com"
+ }
+ },
+ "invocations": [
+ {
+ "commandLine":
+ "frama-c -check tests/sarif/cwe125.c -save tests/sarif/result/cwe125_parse.sav",
+ "arguments": [
+ "-check", "tests/sarif/cwe125.c", "-save",
+ "tests/sarif/result/cwe125_parse.sav"
+ ],
+ "exitCode": 0,
+ "executionSuccessful": true
+ },
+ {
+ "commandLine":
+ "frama-c -check -load tests/sarif/result/cwe125_parse.sav -eva -save tests/sarif/result/cwe125_eva.sav",
+ "arguments": [
+ "-check", "-load", "tests/sarif/result/cwe125_parse.sav", "-eva",
+ "-save", "tests/sarif/result/cwe125_eva.sav"
+ ],
+ "exitCode": 0,
+ "executionSuccessful": true
+ },
+ {
+ "commandLine":
+ "frama-c -check -load tests/sarif/result/cwe125_eva.sav -then -mdr-out tests/sarif/result/cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
+ "arguments": [
+ "-check", "-load", "tests/sarif/result/cwe125_eva.sav", "-then",
+ "-mdr-out", "tests/sarif/result/cwe125.sarif", "-mdr-gen",
+ "sarif", "-mdr-no-print-libc", "-mdr-sarif-deterministic"
+ ],
+ "exitCode": 0,
+ "executionSuccessful": true
+ },
+ {
+ "commandLine":
+ "frama-c -check -load tests/sarif/result/cwe125_eva.sav -then -mdr-out tests/sarif/result/cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
+ "arguments": [
+ "-check", "-load", "tests/sarif/result/cwe125_eva.sav", "-then",
+ "-mdr-out", "tests/sarif/result/cwe125.sarif", "-mdr-gen",
+ "sarif", "-mdr-no-print-libc", "-mdr-sarif-deterministic"
+ ],
+ "exitCode": 0,
+ "executionSuccessful": true
+ }
+ ],
+ "originalUriBaseIds": {
+ "FRAMAC_SHARE": {
+ "uri": "file:///omitted-for-deterministic-output/"
+ },
+ "FRAMAC_LIB": { "uri": "file:///omitted-for-deterministic-output/" },
+ "FRAMAC_PLUGIN": {
+ "uri": "file:///omitted-for-deterministic-output/"
+ },
+ "PWD": { "uri": "file:///omitted-for-deterministic-output/" }
+ },
+ "artifacts": [
+ {
+ "location": { "uri": "tests/sarif/cwe125.c", "uriBaseId": "PWD" },
+ "roles": [ "analysisTarget" ],
+ "mimeType": "text/x-csrc"
+ }
+ ],
+ "results": [
+ {
+ "ruleId": "mem_access",
+ "kind": "open",
+ "level": "none",
+ "message": {
+ "text": "mem_access.",
+ "markdown":
+ "mem_access:\n\n```acsl\nassert mem_access: \\valid_read(array + index);\n```\n\n\n\nThis alarm represents a potential Invalid pointer dereferencing."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "tests/sarif/cwe125.c",
+ "uriBaseId": "PWD"
+ },
+ "region": {
+ "startLine": 21,
+ "startColumn": 8,
+ "endLine": 21,
+ "endColumn": 20,
+ "byteLength": 12
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "mem_access",
+ "level": "error",
+ "message": {
+ "text": "mem_access.",
+ "markdown":
+ "mem_access:\n\n```acsl\nassert mem_access: \\valid_read(array + index);\n```\n\n\n\nThis alarm represents a potential Invalid pointer dereferencing."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "tests/sarif/cwe125.c",
+ "uriBaseId": "PWD"
+ },
+ "region": {
+ "startLine": 27,
+ "endLine": 27,
+ "endColumn": 38,
+ "byteLength": 38
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function printf." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "tests/sarif/cwe125.c",
+ "uriBaseId": "PWD"
+ },
+ "region": {
+ "startLine": 27,
+ "endLine": 27,
+ "endColumn": 6,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "specialization of order at stmt 10." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "tests/sarif/cwe125.c",
+ "uriBaseId": "PWD"
+ },
+ "region": {
+ "startLine": 36,
+ "startColumn": 13,
+ "endLine": 36,
+ "endColumn": 37,
+ "byteLength": 24
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function printf."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "tests/sarif/cwe125.c",
+ "uriBaseId": "PWD"
+ },
+ "region": {
+ "startLine": 27,
+ "endLine": 27,
+ "endColumn": 6,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function printf." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "tests/sarif/cwe125.c",
+ "uriBaseId": "PWD"
+ },
+ "region": {
+ "startLine": 27,
+ "endLine": 27,
+ "endColumn": 6,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "reachability of stmt line 27 in getValueFromArray."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "tests/sarif/cwe125.c",
+ "uriBaseId": "PWD"
+ },
+ "region": {
+ "startLine": 27,
+ "endLine": 27,
+ "endColumn": 38,
+ "byteLength": 38
+ }
+ }
+ }
+ ]
+ }
+ ],
+ "defaultSourceLanguage": "C",
+ "taxonomies": [
+ {
+ "name": "frama-c",
+ "rules": [
+ {
+ "id": "user-spec",
+ "shortDescription": {
+ "text": "User-written ACSL specification."
+ }
+ },
+ {
+ "id": "mem_access",
+ "shortDescription": {
+ "text": "Invalid pointer dereferencing."
+ }
+ }
+ ],
+ "contents": [ "nonLocalizedData" ]
+ }
+ ]
+ }
+ ]
+}
\ No newline at end of file