Commands
checker-framework-3.42.0-eisop3/checker/bin/javac -processor nullness TestNullable.java
Inputs
// TestNullable.java
package test;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
final class TestNullable {
private @MonotonicNonNull String value = null;
@RequiresNonNull({"value"})
void print() {
System.out.println(value);
}
void func() {
if (value == null) {
return;
}
Runnable r = () ->print();
}
}Outputs
TestNullable.java:19: error: [contracts.precondition.not.satisfied] precondition of print is not satisfied.
Runnable r = () -> print();
^
found : this.value is @MonotonicNonNull
required: this.value is @NonNull
Expectation
Similar code with print(); instead of Runnable r = () -> print(); is allowed in current version of checker framework. Checker framework should allow both version of the code, regardless if this is captured by a lambda or not.
Commands
checker-framework-3.42.0-eisop3/checker/bin/javac -processor nullness TestNullable.javaInputs
Outputs
Expectation
Similar code with
print();instead ofRunnable r = () -> print();is allowed in current version of checker framework. Checker framework should allow both version of the code, regardless ifthisis captured by a lambda or not.