diff --git a/checker/tests/resourceleak/LemmaStack.java b/checker/tests/resourceleak/LemmaStack.java new file mode 100644 index 00000000000..e52ff506a51 --- /dev/null +++ b/checker/tests/resourceleak/LemmaStack.java @@ -0,0 +1,48 @@ +// Test case for issue #5175: https://github.com/typetools/checker-framework/issues/5175 +// @skip-test until the issue is fixed + +// The Resource Leak Checker issues the following error: +// LemmaStack.java:40: 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 error + +import java.io.Closeable; +import java.io.IOException; +import java.io.PrintWriter; +import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; +import org.checkerframework.checker.mustcall.qual.CreatesMustCallFor; +import org.checkerframework.checker.mustcall.qual.MustCall; +import org.checkerframework.checker.mustcall.qual.Owning; +import org.checkerframework.checker.nullness.qual.EnsuresNonNull; + +@MustCall("close") public class LemmaStack implements Closeable { + + private @Owning @MustCall("close") PrintWriter session; + + @CreatesMustCallFor("this") + @EnsuresNonNull("session") + private void startProver() { + try { + if (session != null) { + session.close(); + } + session = new PrintWriter("filename.txt"); + } catch (IOException e) { + throw new Error(e); + } + } + + public LemmaStack() { + startProver(); + } + + @EnsuresCalledMethods(value = "session", methods = "close") + @Override + public void close(LemmaStack this) { + session.close(); + } +}