diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 47547bb9e..2002790a7 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -56,47 +56,74 @@ let immediate_or_first_call calling_context (trace : Trace.t) = let get_message diagnostic = let pulse_start_msg = "Pulse found a potential" in match diagnostic with - | AccessToInvalidAddress {calling_context; invalidation_trace; access_trace} -> - (* The goal is to get one of the following messages depending on the scenario: + | 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: - 42: delete x; return x->f - "`x->f` accesses `x`, which was invalidated at line 42 by `delete` on `x`" + 42: delete x; return x->f + "`x->f` accesses `x`, which was invalidated at line 42 by `delete` on `x`" - 42: bar(x); return x->f - "`x->f` accesses `x`, which was invalidated at line 42 by `delete` on `x` in call to `bar`" + 42: bar(x); return x->f + "`x->f` accesses `x`, which was invalidated at line 42 by `delete` on `x` in call to `bar`" - 42: bar(x); foo(x); - "call to `foo` eventually accesses `x->f` but `x` was invalidated at line 42 by `delete` on `x` in call to `bar`" + 42: bar(x); foo(x); + "call to `foo` eventually accesses `x->f` but `x` was invalidated at line 42 by `delete` on `x` in call to `bar`" - If we don't have "x->f" but instead some non-user-visible expression, then - "access to `x`, which was invalidated at line 42 by `delete` on `x`" + If we don't have "x->f" but instead some non-user-visible expression, then + "access to `x`, which was invalidated at line 42 by `delete` on `x`" - Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then - "`x->f` accesses `x`, which was invalidated at line 42 by `delete`" - *) - 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 + Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then + "`x->f` accesses `x`, which was invalidated at line 42 by `delete`" + *) + let pp_access_trace fmt (trace : Trace.t) = + match immediate_or_first_call calling_context trace with + | `Immediate -> + F.fprintf fmt "accessing memory that " + | `Call f -> + F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f + in + let pp_invalidation_trace line invalidation 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 "%a%a" Invalidation.describe invalidation pp_line line + | `Call f -> + F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe + invalidation pp_line line CallEvent.describe f + in + let invalidation_line = + let {Location.line; _} = Trace.get_outer_location invalidation_trace in + line + in + F.asprintf "%a%a" pp_access_trace access_trace + (pp_invalidation_trace invalidation_line invalidation) + invalidation_trace ) | MemoryLeak {procname; location; allocation_trace} -> let allocation_line = let {Location.line; _} = Trace.get_outer_location allocation_trace in