@ -56,7 +56,34 @@ let immediate_or_first_call calling_context (trace : Trace.t) =
let get_message diagnostic =
let get_message diagnostic =
let pulse_start_msg = " Pulse found a potential " in
let pulse_start_msg = " Pulse found a potential " in
match diagnostic with
match diagnostic with
| AccessToInvalidAddress { calling_context ; invalidation_trace ; access_trace } ->
| AccessToInvalidAddress { calling_context ; invalidation ; invalidation_trace ; access_trace } -> (
match invalidation with
| ConstantDereference i when IntLit . equal i IntLit . zero ->
(* Special error message for nullptr dereference *)
let pp_access_trace fmt ( trace : Trace . t ) =
match immediate_or_first_call calling_context trace with
| ` Immediate ->
()
| ` Call f ->
F . fprintf fmt " in call to %a " CallEvent . describe f
in
let pp_invalidation_trace line fmt ( trace : Trace . t ) =
let pp_line fmt line = F . fprintf fmt " on line %d " line in
match immediate_or_first_call calling_context trace with
| ` Immediate ->
F . fprintf fmt " null pointer dereference %a " pp_line line
| ` Call f ->
F . fprintf fmt " null pointer dereference %a indirectly during the call to %a " pp_line
line CallEvent . describe f
in
let invalidation_line =
let { Location . line ; _ } = Trace . get_outer_location invalidation_trace in
line
in
F . asprintf " %s %a%a. " pulse_start_msg
( pp_invalidation_trace invalidation_line )
invalidation_trace pp_access_trace access_trace
| _ ->
(* The goal is to get one of the following messages depending on the scenario:
(* The goal is to get one of the following messages depending on the scenario:
42 : delete x ; return x -> f
42 : delete x ; return x -> f
@ -77,26 +104,26 @@ let get_message diagnostic =
let pp_access_trace fmt ( trace : Trace . t ) =
let pp_access_trace fmt ( trace : Trace . t ) =
match immediate_or_first_call calling_context trace with
match immediate_or_first_call calling_context trace with
| ` Immediate ->
| ` Immediate ->
()
F . fprintf fmt " accessing memory that "
| ` Call f ->
| ` Call f ->
F . fprintf fmt " in call to %a " CallEvent . describe f
F . fprintf fmt " call to %a eventually accesses memory that " CallEvent . describe f
in
in
let pp_invalidation_trace line fmt ( trace : Trace . t ) =
let pp_invalidation_trace line invalidation fmt ( trace : Trace . t ) =
let pp_line fmt line = F . fprintf fmt " on line %d " line in
let pp_line fmt line = F . fprintf fmt " on line %d " line in
match immediate_or_first_call calling_context trace with
match immediate_or_first_call calling_context trace with
| ` Immediate ->
| ` Immediate ->
F . fprintf fmt " null pointer dereference %a" pp_line line
F . fprintf fmt " %a%a" Invalidation . describe invalidation pp_line line
| ` Call f ->
| ` Call f ->
F . fprintf fmt " null pointer dereference %a indirectly during the call to %a" pp_lin e
F . fprintf fmt " %a%a indirectly during the call to %a" Invalidation . describ e
line CallEvent . describe f
invalidation pp_line line CallEvent . describe f
in
in
let invalidation_line =
let invalidation_line =
let { Location . line ; _ } = Trace . get_outer_location invalidation_trace in
let { Location . line ; _ } = Trace . get_outer_location invalidation_trace in
line
line
in
in
F . asprintf " % s %a%a." pulse_start_msg
F . asprintf " % a%a" pp_access_trace access_trace
( pp_invalidation_trace invalidation_line )
( pp_invalidation_trace invalidation_line invalidation )
invalidation_trace pp_access_trace access_trace
invalidation_trace )
| MemoryLeak { procname ; location ; allocation_trace } ->
| MemoryLeak { procname ; location ; allocation_trace } ->
let allocation_line =
let allocation_line =
let { Location . line ; _ } = Trace . get_outer_location allocation_trace in
let { Location . line ; _ } = Trace . get_outer_location allocation_trace in