You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Consider the following code, which appears in checker/tests/resourceleak/LemmaStack.java:
// The Resource Leak Checker issues the following error:// LemmaStack.java:37: error: [reset.not.owning] Calling method startProver resets the must-call// obligations of the expression this, which is non-owning. Either annotate its declaration with an// @Owning annotation, extract it into a local variable, or write a corresponding// @CreatesMustCallFor annotation on the method that encloses this statement.// startProver();// ^// 1 errorimportjava.io.Closeable;
importjava.io.IOException;
importjava.io.PrintWriter;
importorg.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
importorg.checkerframework.checker.mustcall.qual.CreatesMustCallFor;
importorg.checkerframework.checker.mustcall.qual.MustCall;
importorg.checkerframework.checker.mustcall.qual.Owning;
importorg.checkerframework.checker.nullness.qual.EnsuresNonNull;
@MustCall("close") publicclassLemmaStackimplementsCloseable {
private@Owning@MustCall("close") PrintWritersession;
@CreatesMustCallFor("this")
@EnsuresNonNull("session")
privatevoidstartProver() {
try {
if (session != null) {
session.close();
}
session = newPrintWriter("filename.txt");
} catch (IOExceptione) {
thrownewError(e);
}
}
publicLemmaStack() {
startProver();
}
@EnsuresCalledMethods(value = "session", methods = "close")
@Overridepublicvoidclose(LemmaStackthis) {
session.close();
}
}
None of the three suggestions in the error messages works.
annotate its declaration with an @Owning annotation: there is no declaration of this to annotate
extract it into a local variable : @Owning cannot be written on a local variable
write a corresponding @CreatesMustCallFor annotation on the method that encloses this statement: that does not work for the constructor.
The message should be improved to only make suggestions that are possible.
Furthermore, this false negative warning should be eliminated.
The text was updated successfully, but these errors were encountered:
Consider the following code, which appears in
checker/tests/resourceleak/LemmaStack.java
:None of the three suggestions in the error messages works.
@Owning
annotation: there is no declaration ofthis
to annotate@Owning
cannot be written on a local variable@CreatesMustCallFor
annotation on the method that encloses this statement: that does not work for the constructor.The message should be improved to only make suggestions that are possible.
Furthermore, this false negative warning should be eliminated.
The text was updated successfully, but these errors were encountered: