typetools / typetools/checker-framework

@EnsuresNonNullIf produce contracts.conditional.postcondition error

Open
#6,288 0 comments 0 reactions 1 assignee View on GitHub

@smillst is already working on this.

Since Nov 15, 2023.

Dominant language
Java
Stars
1.1k
Forks
440
Avg merge
1d 12h
Merged PRs (30d)
134

Description

I have two methods in utilityclass

    @EnsuresNonNullIf(expression = "#1", result = true)
    public static boolean isOne(@Nullable Integer value) {
        return Objects.equals(value, 1);
    }

    @EnsuresNonNullIf(expression = "#1", result = true)
    public static boolean isOneOrZero(@Nullable Integer value) {
        return Objects.equals(value, 0) || Objects.equals(value, 1);
    }

After I added annotation @EnsuresNonNullIf(expression = "#1", result = true) I get the errors

 error: [contracts.conditional.postcondition] conditional postcondition is not satisfied when isOne returns true.
        return Objects.equals(value, 1);
        ^
  found   : value is @Nullable
  required: value is @NonNull
  
  error: [contracts.conditional.postcondition] conditional postcondition is not satisfied when isOneOrZero returns true.
        return Objects.equals(value, 0) || Objects.equals(value, 1);
        ^
  found   : value is @Nullable
  required: value is @NonNull

Objects.equals -> from jdk package java.util

I added jdk.astub file

import org.checkerframework.checker.nullness.qual.Nullable;

package java.util;

public final class Objects {
    public static boolean equals(@Nullable Object a, @Nullable Object b);
}

but it doesn't help.

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.