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

@@ -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()];
+        }
+    }
+
+}

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",

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)",
+    "procedure": "int NullPointerExceptions.nullListFiles(String)",
-    "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
+    "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
-    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION"
+    "bug_type": "NULL_DEREFERENCE"
   },
   {
     "procedure": "void ContextLeaks.directLeak()",

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
+  }
+
 }

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,