From f2ba1b1c76ca90e78859dbae20386d818ab25890 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2015 09:20:02 -0800
Subject: [PATCH] Add model for java.io.File.listFiles

Reviewed By: jvillard, cristianoc

Differential Revision: D2647011

fb-gh-sync-id: fb23901
---
 infer/models/java/src/java/io/File.java       | 25 +++++++++++++++++++
 infer/tests/ant_report.json                   |  5 ++++
 infer/tests/buck_report.json                  | 11 +++++---
 .../java/infer/NullPointerExceptions.java     |  6 +++++
 .../java/infer/NullPointerExceptionTest.java  |  3 ++-
 5 files changed, 46 insertions(+), 4 deletions(-)
 create mode 100644 infer/models/java/src/java/io/File.java

diff --git a/infer/models/java/src/java/io/File.java b/infer/models/java/src/java/io/File.java
new file mode 100644
index 000000000..1812775e4
--- /dev/null
+++ b/infer/models/java/src/java/io/File.java
@@ -0,0 +1,25 @@
+/*
+* Copyright (c) 2015 - present Facebook, Inc.
+* All rights reserved.
+*
+* This source code is licensed under the BSD style license found in the
+* LICENSE file in the root directory of this source tree. An additional grant
+* of patent rights can be found in the PATENTS file in the same directory.
+*/
+
+package java.io;
+
+import com.facebook.infer.models.InferUndefined;
+import javax.annotation.Nullable;
+
+public class File {
+
+    public @Nullable File[] listFiles() {
+        if (InferUndefined.boolean_undefined()) {
+            return null;
+        } else {
+            return new File[InferUndefined.int_undefined()];
+        }
+    }
+
+}
diff --git a/infer/tests/ant_report.json b/infer/tests/ant_report.json
index e818fefd8..977ea3cc6 100644
--- a/infer/tests/ant_report.json
+++ b/infer/tests/ant_report.json
@@ -354,6 +354,11 @@
     "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
     "bug_type": "NULL_DEREFERENCE"
   },
+  {
+    "procedure": "int NullPointerExceptions.nullListFiles(String)",
+    "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
+    "bug_type": "NULL_DEREFERENCE"
+  },
   {
     "procedure": "void ReaderLeaks.readerNotClosedAfterRead()",
     "file": "codetoanalyze/java/infer/ReaderLeaks.java",
diff --git a/infer/tests/buck_report.json b/infer/tests/buck_report.json
index 6ab2c793a..f41b918ae 100644
--- a/infer/tests/buck_report.json
+++ b/infer/tests/buck_report.json
@@ -464,6 +464,11 @@
     "file": "infer/tests/codetoanalyze/java/infer/ResourceLeaks.java",
     "bug_type": "RESOURCE_LEAK"
   },
+  {
+    "procedure": "String TaintExample.taintToExternalFormEquals(String)",
+    "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION"
+  },
   {
     "procedure": "String TaintExample.taintGetAuthorityStartsWith(String)",
     "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
@@ -550,9 +555,9 @@
     "bug_type": "NULL_DEREFERENCE"
   },
   {
-    "procedure": "String TaintExample.taintToExternalFormEquals(String)",
-    "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
-    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION"
+    "procedure": "int NullPointerExceptions.nullListFiles(String)",
+    "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
+    "bug_type": "NULL_DEREFERENCE"
   },
   {
     "procedure": "void ContextLeaks.directLeak()",
diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
index 71a05c679..764fad52a 100644
--- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
+++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
@@ -430,4 +430,10 @@ public class NullPointerExceptions {
     o.toString();
   }
 
+  int nullListFiles(String pathname) {
+    File dir = new File(pathname);
+    File[] files = dir.listFiles();
+    return files.length; // expect possible NullPointerException as files == null is possible
+  }
+
 }
diff --git a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java
index eeb520016..31c435c79 100644
--- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java
+++ b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java
@@ -64,7 +64,8 @@ public class NullPointerExceptionTest {
         "derefNullableGetter",
         "testSystemGetPropertyArgument",
         "testSystemGetPropertyReturn",
-        "derefNull"
+        "derefNull",
+        "nullListFiles"
     };
     assertThat(
         "Results should contain " + NULL_DEREFERENCE,