Add estimated cost to trace element

Reviewed By: mbouaziz

Differential Revision: D7414240

fbshipit-source-id: b30e4d1
master
Ezgi Çiçek 7 years ago committed by Facebook Github Bot
parent b335fb9c50
commit 872daf1ba7

@ -419,17 +419,18 @@ module TransferFunctionsWCET (CFG : ProcCfg.S) = struct
let report_cost summary instr (cost: Itv.Bound.t) nid reported_so_far =
let mk_message () =
F.asprintf
"The excetution time from the beginning of the function up to this program point is \
likely above the acceptable threshold of %a (estimated cost %a)" Itv.Bound.pp
expensive_threshold Itv.Bound.pp cost
"The execution time from the beginning of the function up to this program point is likely \
above the acceptable threshold of %a (estimated cost %a)" Itv.Bound.pp expensive_threshold
Itv.Bound.pp cost
in
match cost with
| b when Itv.Bound.is_not_infty b
-> (
let above_expensive_threshold = not (Itv.Bound.le cost expensive_threshold) in
let cost_desc = F.asprintf "with estimated cost %a" Itv.Bound.pp cost in
match instr with
| Sil.Call (_, _, _, loc, _) when above_expensive_threshold ->
let ltr = [Errlog.make_trace_element 0 loc "" []] in
let ltr = [Errlog.make_trace_element 0 loc cost_desc []] in
let exn =
Exceptions.Checkers
(IssueType.expensive_execution_time_call, Localise.verbatim_desc (mk_message ()))
@ -441,7 +442,7 @@ module TransferFunctionsWCET (CFG : ProcCfg.S) = struct
| Sil.Call (_, _, _, loc, _)
| Sil.Prune (_, loc, _, _)
when above_expensive_threshold ->
let ltr = [Errlog.make_trace_element 0 loc "" []] in
let ltr = [Errlog.make_trace_element 0 loc cost_desc []] in
let exn =
Exceptions.Checkers
(IssueType.expensive_execution_time_call, Localise.verbatim_desc (mk_message ()))

@ -1,7 +1,7 @@
codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, []
codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, []
codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, []
codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, []
codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, []
codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, []
codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, []
codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002]
codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002]
codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1004]
codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1104]
codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1104]
codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1106]
codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 212]

Loading…
Cancel
Save