From 8b6b77c2573d41da2c355a5bcbc87f624db4d962 Mon Sep 17 00:00:00 2001
From: Michael Ernst <mernst@cs.washington.edu>
Date: Fri, 10 Apr 2026 23:05:54 -0700
Subject: [PATCH 1/2] FAQ about type refinement from initializers into
 constructors

---
 docs/manual/faq.tex | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/docs/manual/faq.tex b/docs/manual/faq.tex
index d5832002d0e..d5a292a3d6e 100644
--- a/docs/manual/faq.tex
+++ b/docs/manual/faq.tex
@@ -54,6 +54,7 @@
 \\ \ref{faq-false-positive}: What is a ``false positive'' warning?
 \\ \ref{faq-false-positive-extend-checker-framework}: How can I improve the Checker Framework to eliminate a false positive warning?
 \\ \ref{faq-infer-fields}: Why doesn't the Checker Framework infer types for fields and method return types?
+\\ \ref{faq-field-initializers}: Why are some operations legal in constructors but not in methods?
 \\ \ref{faq-relationships-between-variables}: Why doesn't the Checker Framework track relationships between variables?
 \\ \ref{faq-path-sensitive}: Why isn't the Checker Framework path-sensitive?
 
@@ -874,6 +875,40 @@
 % programmers see inconsistent results, they should write types explicitly.
 
 
+\subsectionAndLabel{Why are some operations legal in constructors but not in methods?}{faq-field-initializers}
+
+Java permits you to initialize an instance field either in the constructor
+or in a field initializer.  The Checker Framework behaves as if the field
+initializer assignments are performed at the beginning of the constructor,
+because that is how Java executes the program.
+
+Here is an example:
+
+\begin{Verbatim}
+class MyClass1 {
+  @Nullable Object field;
+  MyClass() {
+    field = new Object();
+    field.toString(); // no possible NullPointerException
+  }
+}
+
+class MyClass2 {
+  @Nullable Object field = new Object(); // Same initialization as for MyClass1
+  MyClass() {
+    field.toString(); // no possible NullPointerException
+  }
+}
+
+class MyClass3 {
+  @Nullable Object field;
+  void myMethod() {
+    field.toString(); // Nullness Checker warns: possible NullPointerException
+  }
+}
+\end{Verbatim}
+
+
 \subsectionAndLabel{Why doesn't the Checker Framework track relationships between variables?}{faq-relationships-between-variables}
 
 The Checker Framework estimates the possible run-time value of each

From 9626463ee173dfc11b71ae33b086169c5baff356 Mon Sep 17 00:00:00 2001
From: Michael Ernst <mernst@cs.washington.edu>
Date: Fri, 10 Apr 2026 23:40:31 -0700
Subject: [PATCH 2/2] CodeRabbit

---
 docs/manual/faq.tex | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/docs/manual/faq.tex b/docs/manual/faq.tex
index d5a292a3d6e..d59f86e6ecc 100644
--- a/docs/manual/faq.tex
+++ b/docs/manual/faq.tex
@@ -879,15 +879,16 @@
 
 Java permits you to initialize an instance field either in the constructor
 or in a field initializer.  The Checker Framework behaves as if the field
-initializer assignments are performed at the beginning of the constructor,
-because that is how Java executes the program.
+initializer assignments are performed at the beginning of the constructor
+(after superclass construction), because that is how Java executes the
+program.
 
 Here is an example:
 
 \begin{Verbatim}
 class MyClass1 {
   @Nullable Object field;
-  MyClass() {
+  MyClass1() {
     field = new Object();
     field.toString(); // no possible NullPointerException
   }
@@ -895,7 +896,7 @@
 
 class MyClass2 {
   @Nullable Object field = new Object(); // Same initialization as for MyClass1
-  MyClass() {
+  MyClass2() {
     field.toString(); // no possible NullPointerException
   }
 }
@@ -908,6 +909,9 @@
 }
 \end{Verbatim}
 
+For consistency, the Checker Framework treats the \<MyClass1> and
+\<MyClass2> constructors the same.
+
 
 \subsectionAndLabel{Why doesn't the Checker Framework track relationships between variables?}{faq-relationships-between-variables}