From a89d88063d4e8ba9dcbabb1c72d66c75b4fc8f8e Mon Sep 17 00:00:00 2001
From: Loc Le <quangll@fb.com>
Date: Tue, 6 Apr 2021 10:26:51 -0700
Subject: [PATCH] [pulse][isl] abduction for null case

Reviewed By: skcho

Differential Revision: D27595100

fbshipit-source-id: 1e75c9d30
---
 infer/src/pulse/PulseAbductiveDomain.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 905cd04cc..0390e5557 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -362,9 +362,7 @@ module AddressAttributes = struct
                 Attribute.Invalid (Invalidation.ConstantDereference IntLit.zero, access_trace)
               in
               let null_astate = add_one addr null_attr astate in
-              let null_astate =
-                if is_eq_null then null_astate else abduce_attribute addr null_attr null_astate
-              in
+              let null_astate = abduce_attribute addr null_attr null_astate in
               if null_noop then [Ok null_astate] else [Error (`ISLError null_astate)]
           in
           if is_eq_null then null_astates