[pulse][minor] do not record abstract address in diagnostics

Summary:
This is basically unused except for debugging and is going to cause
issues later.

Reviewed By: mbouaziz

Differential Revision: D14258490

fbshipit-source-id: b2800990e

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
+      ; trace: PulseTrace.t }
-      ; address: AbstractAddress.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} ->
+  | AccessToInvalidAddress {accessed_by; invalidated_by; trace} ->
-      let pp_debug_address f =
+      F.asprintf "`%a` accesses address %a%a past its lifetime" HilExp.AccessExpression.pp
-        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
         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"

infer/src/checkers/PulseDiagnostic.mli

@@ -13,8 +13,7 @@ type t =
   | AccessToInvalidAddress of
       { invalidated_by: PulseInvalidation.t
       ; accessed_by: actor
-      ; trace: PulseTrace.t
+      ; trace: PulseTrace.t }
-      ; address: PulseDomain.AbstractAddress.t }
   | StackVariableAddressEscape of {variable: Var.t; location: Location.t}
 
 val get_message : t -> string

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

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
+      Error (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; trace})
-        (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address; trace})
   | None ->
       Ok astate