search

barry-m / checker-framework

Automatically exported from code.google.com/p/checker-framework
Other
0 stars 0 forks source link

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

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
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

GoogleCodeExporter commented 9 years ago

Original comment by stefanheule@gmail.com on 22 Aug 2013 at 10:26

GoogleCodeExporter commented 9 years ago 
There is a test case in file checkers/tests/nullness/RawField.java

Original comment by mer...@cs.washington.edu on 23 Aug 2013 at 2:50