Permit constructor invocation to return @Initialized, even if an argument is non-@Initialized

Currently the Nullness Checker follows the Freedom-Before-Commitment rules
for constructor invocations:  If all the arguments to the constructor are
@Initialized, then the constructor result is @Initialized.  Otherwise the
new object, which is presumed to have stored arguments in its internal
state, might not have finished initialization, and is thus
@UnknownInitialization.

This behavior is unnecessarily restrictive.  If an @UnknownInitialization
formal parameter is stored only in an @UnknownInitialization field, then
the constructor result can safely be considered @Initialized.  (The
Freedom-Before-Commitment rules don't allow an @UnknownInitialization
field, but our implementation is more flexible and permits this use case).

The Nullness Checker should permit a formal parameter to be marked
indicating that it is only stored in an @UnknownInitialization field.
Possible names for the formal parameter annotation are:
  @NotEventuallyInitialized
  @NotPartOfInitializationState
  @OutsideInitializedState 
  @Uninitialized
  @UninitializedState
  @UninitializedField

The rules could be:
 * a parameter marked as @UninitializedField must obey all subtyping rules
   even within the constructor.
   (Currently, the Nullness Checker permits a constructor to perform
   type-unsafe assignments into fields:  an @UnknownInitialization or
   @UnderInitialization value may be stored into an @Initialized field even
   though this violates the type system.  That is safe under the more
   restrictive FBC rules that forbid @UnknownInitialization fields, but it
   is our goal to permit such fields.)
 * a parameter marked as @UninitializedField may only be stored in a field
   or passed to another @UninitializedField formal parameter.

This comes up in plume-lib's Options class, when making an OptionsInfo
object that has an @UnknownInitialization field.

Original issue reported on code.google.com by michael.ernst@gmail.com on 21 May 2013 at 4:27

Start with the Nullness Checker’s Freedom-Before-Commitment handling for constructor invocations and review how @UnknownInitialization fields and formal parameters are represented. Compare the proposed annotation names and storage rules with the Options class use case in plume-lib. Done means a chosen annotation and specified checking rules permit the safe constructor result while preserving subtyping constraints.