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
Original issue reported on code.google.com by
michael.ernst@gmail.com
on 21 May 2013 at 4:27