From db7dd5aebe617d20337baea759562b19b8f16b56 Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Thu, 12 Nov 2015 11:15:09 -0800
Subject: [PATCH] fixing angelic in case where unknown function is called
 indirectly

Reviewed By: jeremydubreil

Differential Revision: D2644645

fb-gh-sync-id: 65f67e8
---
 infer/src/backend/symExec.ml                     |  1 +
 .../java/infer/NullPointerExceptions.java        | 16 ++++++++++++++++
 2 files changed, 17 insertions(+)

diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index f266e085d..0af319e92 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -1135,6 +1135,7 @@ and add_constraints_on_retval pdesc prop exp typ callee_pname callee_loc =
           IList.fold_left bind_exp prop (Prop.get_sigma prop) in
         (* bind return id to the abducted value pointed to by the pvar we introduced *)
         bind_exp_to_abducted_val exp abducted_ret_pv prop
+        |> add_ret_non_null exp typ
     else add_ret_non_null exp typ prop
 
 and add_constraints_on_actuals_by_ref prop actuals_by_ref callee_pname callee_loc =
diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
index 764fad52a..3a5743125 100644
--- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
+++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
@@ -435,5 +435,21 @@ public class NullPointerExceptions {
     File[] files = dir.listFiles();
     return files.length; // expect possible NullPointerException as files == null is possible
   }
+  
+  native Object unknownFunc();
+
+  Object callUnknownFunc() {
+    return unknownFunc();
+  }
+
+  void dontReportOnNullableDirectReassignmentToUnknown(@Nullable Object o) {
+    o = unknownFunc();
+    o.toString();
+  }
+
+  void dontReportOnNullableIndirectReassignmentToUnknown(@Nullable Object o) {
+    o = callUnknownFunc();
+    o.toString();
+  }
 
 }