diff --git a/infer/src/checkers/PulseDiagnostic.ml b/infer/src/checkers/PulseDiagnostic.ml index dbacd4e54..bdaa2dff0 100644 --- a/infer/src/checkers/PulseDiagnostic.ml +++ b/infer/src/checkers/PulseDiagnostic.ml @@ -7,7 +7,6 @@ open! IStd module F = Format -module AbstractAddress = PulseDomain.AbstractAddress type actor = {access_expr: HilExp.AccessExpression.t; location: Location.t} [@@deriving compare] @@ -15,8 +14,7 @@ type t = | AccessToInvalidAddress of { invalidated_by: PulseInvalidation.t ; accessed_by: actor - ; trace: PulseTrace.t - ; address: AbstractAddress.t } + ; trace: PulseTrace.t } | StackVariableAddressEscape of {variable: Var.t; location: Location.t} let get_location = function @@ -25,13 +23,10 @@ let get_location = function let get_message = function - | AccessToInvalidAddress {accessed_by; invalidated_by; address; trace} -> - let pp_debug_address f = - if Config.debug_mode then F.fprintf f " (debug: %a)" AbstractAddress.pp address - in - F.asprintf "`%a` accesses address %a%a past its lifetime%t" HilExp.AccessExpression.pp + | AccessToInvalidAddress {accessed_by; invalidated_by; trace} -> + F.asprintf "`%a` accesses address %a%a past its lifetime" HilExp.AccessExpression.pp accessed_by.access_expr PulseTrace.pp_interesting_events trace PulseInvalidation.pp - invalidated_by pp_debug_address + invalidated_by | StackVariableAddressEscape {variable} -> let pp_var f var = if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary" diff --git a/infer/src/checkers/PulseDiagnostic.mli b/infer/src/checkers/PulseDiagnostic.mli index e16225d16..380adc139 100644 --- a/infer/src/checkers/PulseDiagnostic.mli +++ b/infer/src/checkers/PulseDiagnostic.mli @@ -13,8 +13,7 @@ type t = | AccessToInvalidAddress of { invalidated_by: PulseInvalidation.t ; accessed_by: actor - ; trace: PulseTrace.t - ; address: PulseDomain.AbstractAddress.t } + ; trace: PulseTrace.t } | StackVariableAddressEscape of {variable: Var.t; location: Location.t} val get_message : t -> string diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 44edefb80..62c97d073 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -24,7 +24,7 @@ module AbstractAddress : sig val init : unit -> unit - val pp : F.formatter -> t -> unit + val pp : F.formatter -> t -> unit [@@warning "-32"] val mk_fresh : unit -> t end diff --git a/infer/src/checkers/PulseOperations.ml b/infer/src/checkers/PulseOperations.ml index 0191205fc..ee9af52a7 100644 --- a/infer/src/checkers/PulseOperations.ml +++ b/infer/src/checkers/PulseOperations.ml @@ -21,8 +21,7 @@ type 'a access_result = ('a, PulseDiagnostic.t) result let check_addr_access actor (address, trace) astate = match Memory.get_invalidation address astate.heap with | Some invalidated_by -> - Error - (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address; trace}) + Error (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; trace}) | None -> Ok astate