Add a complete example of a resource wrapper type to the manual (#6680)

checker/tests/resourceleak/InputStreamWrapper.java

@@ -0,0 +1,27 @@
+import java.io.*;
+import org.checkerframework.checker.calledmethods.qual.*;
+import org.checkerframework.checker.mustcall.qual.*;
+
+@InheritableMustCall("dispose")
+class InputStreamWrapper {
+  private final @Owning InputStream stream;
+
+  @MustCallAlias InputStreamWrapper(@MustCallAlias InputStream stream) {
+    this.stream = stream;
+  }
+
+  @EnsuresCalledMethods(value = "this.stream", methods = "close")
+  public void dispose() throws IOException {
+    this.stream.close();
+  }
+
+  /** Shows that either the stream or the wrapper can be closed. */
+  static void test(@Owning InputStream stream, boolean b) throws IOException {
+    InputStreamWrapper wrapper = new InputStreamWrapper(stream);
+    if (b) {
+      stream.close();
+    } else {
+      wrapper.dispose();
+    }
+  }
+}

docs/manual/resource-leak-checker.tex

@@ -366,6 +366,36 @@
   \<@Owning> field cannot have a resource alias relationship).
 \end{enumerate}
 
+\subsectionAndLabel{A complete wrapper type example}{resource-leak-wrapper-type-example}
+
+Here is a complete example of a type \<InputStreamWrapper> that wraps an \<InputStream> as a resource alias.  Defining a wrapper type typically involves combined usage of \<@InheritableMustCall>, \<@EnsuresCalledMethods>, an \<@Owning> field, and \<@MustCallAlias>.  The \<test> method shows that the checker is able to verify code that releases an \<InputStream> using either the \<InputStream> directly or a wrapping \<InputStreamWrapper>.
+
+\begin{verbatim}
+@InheritableMustCall("dispose")
+class InputStreamWrapper {
+  private final @Owning InputStream stream;
+
+  @MustCallAlias InputStreamWrapper(@MustCallAlias InputStream stream) {
+    this.stream = stream;
+  }
+
+  @EnsuresCalledMethods(value = "this.stream", methods = "close")
+  public void dispose() throws IOException {
+    this.stream.close();
+  }
+
+  /** Shows that either the stream or the wrapper can be closed. */
+  static void test(@Owning InputStream stream, boolean b) throws IOException {
+    InputStreamWrapper wrapper = new InputStreamWrapper(stream);
+    if (b) {
+      stream.close();
+    } else {
+      wrapper.dispose();
+    }
+  }
+}
+\end{verbatim}
+
 
 \sectionAndLabel{Creating obligations (how to re-assign a non-final owning field)}{resource-leak-createsmustcallfor}