Reputation: 1762
How should I deal with lambda functions using checker-framework typed annotations?
For example,
private void dispatch(Progress progress, Load request, @Nullable Layer layer)
{
if (layer == null) return;
Utils.log("DISPATCHING " + layer.name);
JThread.run(() -> runDispatch(progress, request, layer));
}
Checker will issue a argument.type.incompatible
warning on the runDispatch
line call, even though layer
is being checked beforehand. I understand that the lambda function is inside a different context, and therefore Checker can't correctly assess that. What is the best way to deal with it?
Extra info
Full warning:
error: [argument.type.incompatible] incompatible types in argument.
[ERROR] found : @Initialized @Nullable Layer<? extends @Initialized @NonNull Item, ? extends @Initialized @NonNull Deliver, ? extends @Initialized @NonNull Recipient>
[ERROR]
[ERROR] required: @Initialized @NonNull Layer<? extends @Initialized @NonNull Item, ? extends @Initialized @NonNull Deliver, ? extends @Initialized @NonNull Recipient>
runDispatch
is declared on the same class, signature private void runDispatch(Progress progress, Load request, Layer layer)
Another example: Elsewhere in my code I have a similar situation, but involving method behavior:
on Item.class
:
@EnsuresNonNullIf(expression="extraAction", result=true)
public final boolean hasExtraAction() {
return extraAction != null;
}
on a separate class:
@RequiresNonNull("#2.extraAction")
private void buildExtraActionRunnable(Layer layer, Item item, Deliver deliver) {
....
}
...
} else if (item.hasExtraAction()) {
Runnable r = () -> buildExtraActionRunnable(layer, item, deliver);
Here, at the Runnable line I get error: [contracts.precondition.not.satisfied] the called method 'buildExtraActionRunnable(layer, item, deliver)' has a precondition 'item.extraAction' that is not satisfied
Upvotes: 0
Views: 766
Reputation: 8117
I agree that this is a bug in the Nullness Checker. In this part of your code:
Utils.log("DISPATCHING " + layer.name);
JThread.run(() -> runDispatch(progress, request, layer));
the Nullness Checker knows at the call of Utils.log
that layer
is non-null, but it doesn't know that fact at the call to runDispatch
within the method body. Within the method body, it is using the declared type of layer
rather than a refined type computed via dataflow analysis.
Your question was how to work around the Checker Framework bug. One way to do so is to introduce a new variable:
Utils.log("DISPATCHING " + layer.name);
Layer layer2 = layer; // work around CF issue #1248
JThread.run(() -> runDispatch(progress, request, layer2));
The above code typechecks correctly.
I can't give a detailed answer for your second example, because you didn't give a compilable MWE. But whenever there is an error of the form error: [KEY] ...
, you can always suppress it by adding @SuppressWarnings("KEY")
. It your case, this would be @SuppressWarnings("contracts.precondition.not.satisfied")
.
Upvotes: 1