diff --git a/checker/bin-devel/count-suppressions b/checker/bin-devel/count-suppression-reasons
similarity index 91%
rename from checker/bin-devel/count-suppressions
rename to checker/bin-devel/count-suppression-reasons
index 1ca1e143740..f4326b591a9 100755
--- a/checker/bin-devel/count-suppressions
+++ b/checker/bin-devel/count-suppression-reasons
@@ -3,7 +3,7 @@
 # This command counts the approximate frequency of each distinct reason for
 # warning suppressions, in all files under the current directory.
 # To invoke it, pass a type system name; for example:
-#   count-suppressions nullness
+#   count-suppression-reasons nullness
 # The argument to this script is actually a regular expression.
 
 # The "reason" for a warning suppression is the Java line comment after it:
@@ -62,8 +62,8 @@ fi
 # Diagnostics
 # echo "regex=${regex}"
 
-greplines=$(mktemp /tmp/count-suppressions."$(date +%Y%m%d-%H%M%S)"-XXX)
-countedreasons=$(mktemp /tmp/count-suppressions."$(date +%Y%m%d-%H%M%S)"-XXX)
+greplines=$(mktemp /tmp/count-suppression-reasons."$(date +%Y%m%d-%H%M%S)"-XXX)
+countedreasons=$(mktemp /tmp/count-suppression-reasons."$(date +%Y%m%d-%H%M%S)"-XXX)
 
 # These are the two types of matching lines:
 #  * "checkername" or "chekername:..."
@@ -71,10 +71,10 @@ countedreasons=$(mktemp /tmp/count-suppressions."$(date +%Y%m%d-%H%M%S)"-XXX)
 #    include "@SuppressWarnings" because it might appear on the previous line.
 #  * @AssumeAssertion(checkername)
 # This grep command captures a few stray lines; users should ignore them.
-# This grep command assumes that tests are not annotated, and it hard-codes ignoring "annotated-jdk", "jdk", "true positive", "// TP" (as an alias for "true positive"), and "count-suppressions-ignore".
+# This grep command assumes that tests are not annotated, and it hard-codes ignoring "annotated-jdk", "jdk", "true positive", "// TP" (as an alias for "true positive"), and "count-suppression-reasons-ignore".
 ${GREP} -n --recursive --include='*.java' "\"${regex}[:\"]\(.*[^;]\)\?\(\$\|//\)\|@AssumeAssertion(${regex})" \
     | grep -v "@AnnotatedFor" | grep -v "/tests/" \
-    | grep -v "/annotated-jdk/" | grep -v "/jdk/" | grep -v "^jdk/" | grep -v "true positive" | grep -v "// TP" | grep -v "count-suppressions-ignore" > "${greplines}"
+    | grep -v "/annotated-jdk/" | grep -v "/jdk/" | grep -v "^jdk/" | grep -v "true positive" | grep -v "// TP" | grep -v "count-suppression-reasons-ignore" > "${greplines}"
 
 total=$(wc -l < "${greplines}")
 ## Don't output a total, to avoid people using this approximate count.
@@ -87,7 +87,7 @@ cat "${greplines}" \
     | ${SED} 's/ \+$//' \
     | sort | uniq -c | sort -rg > "${countedreasons}"
 
-# Add leading percentages to `uniq -c` output.  Note that it rounds down to the nearest integer.
+# Add leading percentages to `uniq -c` output.  Note that it rounds *down* to the nearest integer.
 # (Digits afert the decimal don't make a practical difference.)
 while read -r line; do
     count=$(echo "$line" | cut -f1 -d " ");
diff --git a/docs/developer/developer-manual.html b/docs/developer/developer-manual.html
index 946039c5c2b..87c80a4d8a6 100644
--- a/docs/developer/developer-manual.html
+++ b/docs/developer/developer-manual.html
@@ -47,6 +47,8 @@ <h1 id="Checker_Framework_developer_manual">Checker Framework developer manual</
       <li><a href="#Documenting_refactoring_ideas">Documenting refactoring ideas</a></li>
       <li><a href="#annotated-library-version-numbers">Version numbers for annotated libraries</a></li>
       <li><a href="#Making_a_Checker_Framework_release">Making a Checker Framework release</a></li>
+      <li><a href="#Case_studies">Describing a case study</a></li>
+      <li><a href="#Counting_annotations">Counting annotations</a></li>
       <li><a href="#Build_historical">Building a historical version of the Checker Framework</a></li>
     </ul>
 <!-- end toc -->
@@ -475,12 +477,70 @@ <h2 id="Making_a_Checker_Framework_release">Making a Checker Framework release</
 </p>
 
 
+<h2 id="Case_studies">Describing a case study</h2>
+
+<p>
+  After you have performed a case study of applying some checker to an
+  open-source codebase, you should have:
+</p>
+
+<ul>
+  <li>
+    the unannotated code, as of the time/commit you started annotating it.
+    This might be in your forked repository, or in an upstream repository.
+  </li>
+  <li>
+    the annotated code.  Typically, this is in a branch of your forked repository.
+
+    <p>
+    In the annotated code, each <code>@SuppressWarnings</code> annotation should have a brief justification, explaining why the code is correct and the warning is a false positive.
+    The justification should be a <code>//</code>-style comment, on the same line as the argument to <code>@SuppressWarnings</code>.  For example:
+    </p>
+
+<pre>
+  @SuppressWarnings("nullness:assignment") // dynamic check: checked against null immediately above
+
+  @SuppressWarnings({
+    "nullness:assignment" // dynamic check: checked against null immediately above
+  })
+</pre>
+
+    If there are more than about 10 warning suppressions, prefix each one by a
+    category followed by a colon (as with "dynamic check:") above, to aid in
+    computing statistics about the causes of false positive warnings.
+
+  </li>
+  <li>
+    the command to run the type-checker(s) on the annotated code.
+  </li>
+  <li>
+    a list of all the bugs you fixed, with a brief description of each.  The
+    description can point to pull requests, or commits, or just be text; provide
+    whatever is most helpful.
+  </li>
+</ul>
+
+
+<h2 id="Counting_annotations">Counting annotations</h2>
+
+<p>
+After you have annotated a project, you may wish to count the annotations that you have written.
+These programs will help you do that:
+</p>
+
+<ul>
+  <li><a href="https://checkerframework.org/api/org/checkerframework/common/util/count/AnnotationStatistics.html">AnnotationStatistics</a></li>
+  <li><a href="https://checkerframework.org/api/org/checkerframework/common/util/count/JavaCodeStatistics.html">JavaCodeStatistics</a></li>
+  <li><a href="https://github.com/typetools/checker-framework/blob/master/checker/bin-devel/count-suppressions">count-suppression-reasons"></a></li>
+</ul>
+
+
 <h2 id="Build_historical">Building a historical version of the Checker Framework</h2>
 
 <p>
 The use of four different repositories, as explained in
 "<a href="#Related_repositories">Related repositories</a>" above, means that you
-cannot check out an old version of the Checker Framework and build it
+cannot just check out an old version of the Checker Framework and build it
 with <code>./gradlew assemble</code>.  By default, the Checker Framework build
 uses the latest version of the other three repositories, which are rarely
 compatible with an old version of the Checker Framework.  One symptom of the
@@ -534,7 +594,7 @@ <h2 id="Build_historical">Building a historical version of the Checker Framework
 </body>
 </html>
 
-<!--  LocalWords:  TODO javacutil gradle javadoc reformats subprojects pre NullAway CircleCI travis ci downarrow dropdown MYUSERID NNN doesn
+<!--  LocalWords:  TODO javacutil gradle javadoc reformats subprojects pre NullAway CircleCI travis ci downarrow dropdown MYUSERID NNN doesn AnnotationStatistics JavaCodeStatistics stubparser
  -->
 <!--  LocalWords:  subproject personalblog changelog config SOMEDOMAIN YAML isn
  -->