typetools / typetools/checker-framework
@EnsuresNonNullIf produce contracts.conditional.postcondition error
Open
@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
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.