Eclipse does not properly override the nullability of the annotations

Monniasza commented 1 year ago

Summary

The nullability annotation @Nullable given on the method1() does not override the @Nonnull on the type argument T

Expected results:

On line 12, there should be a warning about a null pointer dereference: Potential null pointer access: The variable str2 may be null at this location
There should be no warnings on line 11

Actual results:

There are no null analysis warnings on line 12, but there is a warning on line 11: Null type mismatch: required '@Nonnull String' but the provided value is null

Null analysis settings

Setting	Value
Null pointer access	Error
Potential null pointer access	Error
Redundant null check	Warning
Include 'assert' in null analysis	True
Enable annotation-based null analysis	True
Violation of null specification	Error
Conflict between null annotations and null inference	Error
Unchecked conversion from non-annotated to `@NonNull` type	Warning
Unsafe conversion of annotated type to less-annotated type	Info
Problems detected by pessimistic analysis for free type variables	Warning
Unsafe `@Nonnull` interpretation of free type variable from library	Warning
Redundant null annotation	Warning
`@Nonnull` parameter not annotated in overriding method	Warning
Missing `@NonNullByDefault` annotation on package	Warning
Inherit null annotations	True
Enable syntactic null analysis for fields	True
Search for external annotations in all build path locations	True

Nullability annotations

A\T	Primary	Secondary
`@Nonnull`	`javax.annotation.Nonnull`	`org.checkerframework.checker.nullness.qual.NonNull`
`@Nullable`	`javax.annotation.Nullable`	`org.checkerframework.checker.nullness.qual.Nullable`
`@NonNullByDefault`	`javax.annotation.ParametersAreNonnullByDefault`	`org.checkerframework.checker.nullness.qual.ParametersAreNonnullByDefault`

Example using Google's ErrorProne:

import javax.annotation.Nonnull;
import javax.annotation.Nullable;
public class ClassA<@Nonnull T> {
    public @Nullable T method1(@Nullable T input){
        return input;
    }
    public static void main(String[] args){
        ClassA<String> objA = new ClassA<>();
        String str = null;
        //🡓inferred nonnull, expected nullable, warning on the input, even though it is marked nullable🡓
        String str2 = objA.method1(str);
        int len = str2.length(); //no error reported, even though this method would fail with a NPE
    }
}

NPE thrown by the example:

Exception in thread "main" java.lang.NullPointerException
    at ClassA.main(ClassA.java:12)

stephan-herrmann commented 1 year ago

A word of warning, before we analyse the situation in detail:

The annotation javax.annotation.Nonnull is not designed for use against a type parameter like <@Nonnull T>.

If you don't get a compile error right there, then you seem to be using a variant of this annotation that doesn't even have any @Target meta annotation. This situation is strongly discouraged, as the semantics are very likely not what you expect.

Here's the output I get when using proper annotations with @Target(TYPE_USE):

----------
1. WARNING in /tmp/ClassA.java (at line 8)
        ClassA<String> objA = new ClassA<>();
               ^^^^^^
Null constraint mismatch: The type 'String' is not a valid substitute for the type parameter '@NonNull T'
----------
2. INFO in /tmp/ClassA.java (at line 8)
        ClassA<String> objA = new ClassA<>();
                              ^^^^^^^^^^^^^^
Unsafe null type conversion (type annotations): The value of type '@NonNull ClassA<@NonNull String>' is made accessible using the less-annotated type 'ClassA<String>'
----------
3. WARNING in /tmp/ClassA.java (at line 12)
        int len = str2.length(); //no error reported, even though this method would fail with a NPE
            ^^^
The value of the local variable len is not used
----------
4. WARNING in /tmp/ClassA.java (at line 12)
        int len = str2.length(); //no error reported, even though this method would fail with a NPE
                  ^^^^
Potential null pointer access: The variable str2 may be null at this location
----------
4 problems (0 errors, 3 warnings, 1 info)

This looks OK to me.

Monniasza commented 1 year ago

I propose a warning like this for @Nullable used on @Nonnull type arguments: The type argument is @Nonnull, but a @Nullable type is requested

eclipse-jdt / eclipse.jdt.core