Notes on what the Called Methods Checker is actually checking, in the…

… manual

Co-authored-by: Manu Sridharan <msridhar@gmail.com>

docs/manual/called-methods-checker.tex

@@ -6,8 +6,10 @@
 of the form ``call method A before method B''. For the purpose of this
 checker, a method has ``definitely been called'' if it is \emph{invoked}:
 a method that might never return or that might throw an exception has
-a method that might never return or that might throw an exception has
 definitely been called on every path after the call, including exceptional paths.
+The checker also assumes that the program is free of null-pointer dereferences.
+You can verify that all pointer dereferences are safe
+by running the Nullness Checker (Section~\ref{nullness-checker}).
 
 The Called Methods Checker provides built-in support for one such property:
 that clients of the builder pattern for object
@@ -154,7 +156,7 @@
   The bottom type for the Called Methods hierarchy. Conceptually, this annotation
   means that all possible methods have been called on the object. Programmers should rarely,
   if ever, need to write this annotation---write an appropriate \<@CalledMethods> annotation
-  instead.
+  instead. The type of \<null> is \<@CalledMethodsBottom>.
 
 \end{description}