Commit 472692ef authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

Merge branch 'fix/andre/mdr-sarif-duplicate-invocations' into 'master'

[MdR] avoid duplicate invocations in SARIF

See merge request frama-c/frama-c!2906
parents c58df58d 58123e25
......@@ -60,7 +60,19 @@ module Analysis_cmdline =
let command_line () = Array.to_list Sys.argv
let update_cmdline () = Analysis_cmdline.add (command_line())
let update_cmdline =
let already_updated = ref false in
fun () ->
if not (!already_updated) then begin
(* This function must be run after the loading stage, so that
the Analysis_cmdline state contains the list of previous launches
if any. However, `-then` restart the boot sequence from the loading
included, meaning that the hook will be replayed _also_ after each
`-then`. Using a _non-projectified_ boolean ref ensures that we add
the command line only once per run. *)
already_updated := true;
Analysis_cmdline.add (command_line())
end
let () = Cmdline.run_after_loading_stage update_cmdline
......
/* 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@.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
*/
#include "__fc_builtin.h"
......
[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] using specification for function Frama_C_interval
[eva:alarm] tests/sarif/cwe125.c:21: Warning:
out of bounds read. assert \valid_read(array + index);
[eva:alarm] tests/sarif/cwe125.c:27: Warning:
out of bounds read. assert \valid_read(array + index);
[eva] done for function main
[eva] tests/sarif/cwe125.c:27:
assertion 'Eva,mem_access' got final status invalid.
[kernel:annot:missing-spec] tests/sarif/cwe125.c:27: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function getValueFromArray:
value ∈ {0}
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
arr[0..9] ∈ {0}
test ∈ [0..9]
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
2 functions analyzed (out of 2): 100% coverage.
In these functions, 8 statements reached (out of 9): 88% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 0 warnings
by the Frama-C kernel: 0 errors 2 warnings
----------------------------------------------------------------------------
2 alarms generated by the analysis:
2 invalid memory accesses
1 of them is a sure alarm (invalid status).
----------------------------------------------------------------------------
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.
----------------------------------------------------------------------------
[kernel] Parsing tests/sarif/cwe125.c (with preprocessing)
[kernel:typing:implicit-function-declaration] tests/sarif/cwe125.c:27: Warning:
Calling undeclared function printf. Old style K&R code?
......@@ -34,17 +34,6 @@
"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",
......
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