Commit 2b27d0b6 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

Merge branch 'fix/mdr/several-runs' into 'master'

[MdR] keep tracks of all arguments when -save/-load sequences occur

Closes #945

See merge request frama-c/frama-c!2871
parents 79c5b7bc 97a2d825
...@@ -39,7 +39,7 @@ PLUGIN_CMO:=\ ...@@ -39,7 +39,7 @@ PLUGIN_CMO:=\
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE) PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure share/acsl.xml 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 include $(FRAMAC_SHARE)/Makefile.dynamic
......
...@@ -47,24 +47,34 @@ let get_remark remarks label = ...@@ -47,24 +47,34 @@ let get_remark remarks label =
| None -> [] | None -> []
| Some l -> l | 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 = module Analysis_cmdline =
State_builder.Ref(Datatype.List(Datatype.String)) State_builder.List_ref(Datatype.List(Datatype.String))
(struct (struct
let name = "Sarif_gen.Analysis_cmdline" let name = "Sarif_gen.Analysis_cmdline"
let dependencies = [] let dependencies = []
let default = command_line
end) 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 gen_invocation () =
let cl = Analysis_cmdline.get () in let cls = Analysis_cmdline.get () in
(* The first argument is _always_ the binary name, but to avoid printing it let gen_one cl =
as an absolute path to binlevel.opt, we replace it with 'frama-c' *) (* The first argument is _always_ the binary name, but to avoid printing it
let cl = "frama-c" :: List.tl cl in as an absolute path to binlevel.opt, we replace it with 'frama-c' *)
let commandLine = String.concat " " cl in let cl = "frama-c" :: List.tl cl in
let arguments = List.tl cl in let commandLine = String.concat " " cl in
Invocation.create ~commandLine ~arguments () let arguments = List.tl cl in
Invocation.create ~commandLine ~arguments ()
in
List.rev_map gen_one cls
let gen_remark alarm = let gen_remark alarm =
let open Markdown in let open Markdown in
...@@ -215,7 +225,7 @@ let make_taxonomies rules = Datatype.String.Map.fold add_rule rules [] ...@@ -215,7 +225,7 @@ let make_taxonomies rules = Datatype.String.Map.fold add_rule rules []
let gen_run remarks = let gen_run remarks =
let tool = frama_c_sarif () in let tool = frama_c_sarif () in
let name = "frama-c" in let name = "frama-c" in
let invocations = [gen_invocation ()] in let invocations = gen_invocation () in
let rules, results = gen_results remarks in let rules, results = gen_results remarks in
let user_annot_results = gen_statuses () in let user_annot_results = gen_statuses () in
let rules = let rules =
......
/* run.config /* 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 /* extracted from Juliet test suite v1.3 for C
......
...@@ -20,7 +20,7 @@ the `bad` ones have indeed an error. ...@@ -20,7 +20,7 @@ the `bad` ones have indeed an error.
The C source files (not including the headers `.h` files) The C source files (not including the headers `.h` files)
that have been considered during the analysis are the following: 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 ...@@ -60,10 +60,10 @@ Table: Warning reported by Frama-C
| Location | Description | | 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: Message:
...@@ -87,10 +87,10 @@ Table: Alarm emitted by the analysis ...@@ -87,10 +87,10 @@ Table: Alarm emitted by the analysis
| No | Kind | Emitter | Function | Location | | 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 The following ACSL assertion must hold to avoid invalid pointer dereferencing
(undefined behavior). (undefined behavior).
......
[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] Analyzing a complete application starting at main
[eva] Computing initial state [eva] Computing initial state
[eva] Initial state computed [eva] Initial state computed
[eva:initial-state] Values of globals at initialization [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] using specification for function exit
[eva] FRAMAC_SHARE/libc/string.h:118: [eva] FRAMAC_SHARE/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva] tests/eva/cwe126.c:62: starting to merge loop iterations [eva] tests/md/cwe126.c:62: starting to merge loop iterations
[eva] tests/eva/cwe126.c:40: [eva] tests/md/cwe126.c:40:
allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l40 allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l40
[eva] tests/eva/cwe126.c:26: starting to merge loop iterations [eva] tests/md/cwe126.c:26: starting to merge loop iterations
[eva:alarm] tests/eva/cwe126.c:28: Warning: [eva:alarm] tests/md/cwe126.c:28: Warning:
out of bounds read. assert \valid_read(data + i); out of bounds read. assert \valid_read(data + i);
[eva] done for function main [eva] done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
...@@ -54,4 +54,4 @@ ...@@ -54,4 +54,4 @@
Preconditions 8 valid 0 unknown 0 invalid 8 total Preconditions 8 valid 0 unknown 0 invalid 8 total
100% of the logical properties reached have been proven. 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
/* 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);
}
{
"$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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment