/*
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 */

package com.facebook.infer.annotation;

import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;

/**
 * A method annotated with @Initializer should always be be called before the object is used. Users
 * of the class and static checkers must enforce, and can rely on, this invariant. Examples include
 * methods called indirectly by the constructor, protocols of init-then-use where some values are
 * initialized after construction but before the first use, and builder classes where an object
 * initialization must complete before build() is called.
 */
@Retention(RetentionPolicy.CLASS)
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.CONSTRUCTOR, ElementType.METHOD})
public @interface Initializer {}

@@ -432,14 +432,22 @@
 zer 
-should
+is expected to
  alw
@@ -457,15 +457,13 @@
  be 
-be call
+invok
 ed b
@@ -491,215 +491,840 @@
 sed.
- Users%0A * of the clas
+%0A * Nullsafe typechecker respects thi
 s an
-d s
+no
 tati
-c checkers must enforce, and can rely on, this invariant. Examples include%0A * methods called indirectly by the constructor, protocols of init-then-use where some values are%0A *
+on when checking field initialization: if a field is%0A * assigned a (non-nullable) value in @Initializer-annotated method, it is considered initialized,%0A * and hence does not require @Nullable annotation.%0A *%0A * %3Cp%3EMethods annotated as @Initializer should not be private. If the actual initialization is%0A * happening in a private helper method, then the public method that calls this helper method should%0A * be annotated.%0A *%0A * %3Cp%3EIn this example, only field2 will be reported as not initialized:%0A *%0A * %3Cp%3E%3Ccode%3E%0A * class Example %7B%0A *   private String field1;%0A *   private String field2;%0A *   // Will be initialized in finishCreation().%0A *   // (It is a good idea to specify that in comments in your real code!)%0A *   private String field3;%0A *%0A *   public Example() %7B%0A *     field1 = %22OK:
  ini
@@ -1336,13 +1336,14 @@
 zed 
-after
+in the
  con
@@ -1352,131 +1352,406 @@
 ruct
-ion but before the first use, and builder classes where an object%0A * initialization must complete before build() is called.
+or%22;%0A *     // BAD: did not initialize field2!%0A *     // (But OK not to initialize field3).%0A *   %7D%0A *%0A *   // This should be called before the object can be used.%0A *   // It is a good idea to always document @Initializer methods for your client).%0A *   @Initializer%0A *   public void finishCreation() %7B%0A *     field3 = %22OK: Nullsafe assumes this will be called after creation%22;%0A *   %7D%0A * %7D%0A * %3C/code%3E
 %0A */

Improve documentation for @Initializer annotation