From 38435fec03c5be3f92d4e671aaa492236adea231 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Fri, 8 Mar 2019 10:49:32 -0800
Subject: [PATCH] [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  | 13 ++++---------
 infer/src/checkers/PulseDiagnostic.mli |  3 +--
 infer/src/checkers/PulseDomain.mli     |  2 +-
 infer/src/checkers/PulseOperations.ml  |  3 +--
 4 files changed, 7 insertions(+), 14 deletions(-)

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