False Negative: NULL_DEREFERENCE missing for uninitialized object array element dereference

[leemeii]

Describe the bug
Infer fails to report NULL_DEREFERENCE for dereferencing an uninitialized element in a newly created object array, even though the element is null by default and the dereference will cause a runtime NullPointerException.

To Reproduce

import java.lang.ref.Reference;

public class a {

    public static void main(String[] args) {
        reproduceRisk();
    }

    /**
     * Vulnerability: NPE caused by immediate access to newly created object array
     * Logic: Newly created object array slots are all null, immediate dereference will crash.
     */
    public static void reproduceRisk() {
        int index = 0;
        // 1. Create array, index 0 is null
        Reference[] refs = new Reference[1]; // <- array created with null elements
        
        // 2. Direct access and method call
        
        refs[0].get(); // <- should report NULL_DEREFERENCE (FN)
    }
}

Expected behavior
Infer should report a NULL_DEREFERENCE at the line where the array element is dereferenced (e.g., refs[0].get()), since Java object array elements are null by default and dereferencing null throws NullPointerException.

Actual behavior
No issues are reported. The dereference of the null array element is silently ignored.

Java version: JDK 21
How do you use Infer: CLI