A manual's example for @Raw doesn't type check

[GoogleCodeExporter]

What steps will reproduce the problem?
Run the nullness checker on the following example from 
<http://types.cs.washington.edu/checker-framework/current/checkers-manual.html#i
nitialization-rawness-checker>:

public class MyClass {
  Object field1;
  Object field2;
  Object field3;

  public MyClass(String arg1) {
    this.field1 = arg1;
    init_other_fields();
  }

  @EnsuresNonNull({"field2", "field3"})
  private void init_other_fields(@Raw MyClass this) {
    field2 = new Object();
    field3 = new Object();
  }

}

What is the expected output? What do you see instead?
The manual suggests that the above piece of code is valid but the checker 
reports the following problem:

javac -Awarns -processor org.checkerframework.checker.nullness.NullnessChecker 
-d bin src/MyClass.java 
src/MyClass.java:10: warning: [method.invocation.invalid] call to 
init_other_fields() not allowed on the given receiver.
    init_other_fields();
                     ^
  found   : @UnderInitialization(java.lang.Object.class) @NonNull MyClass
  required: @Initialized @NonNull MyClass
1 warning

What version of the product are you using? On what operating system?
1.8.0-jsr308-1.8.0, linux

Original issue reported on code.google.com by reprogra...@gmail.com on 2 May 2014 at 1:13

[GoogleCodeExporter]

I can reproduce your output when using 
org.checkerframework.checker.nullness.NullnessChecker.
However, as the example is about rawness, the right processor is:
org.checkerframework.checker.nullness.NullnessRawnessChecker
Using the NullnessRawnessChecker, the example behaves as expected.

In case this is not explicit, the manual should be updated.

Original comment by wdi...@gmail.com on 2 May 2014 at 2:50

• Changed state: Accepted
• Added labels: Manual

[GoogleCodeExporter]

Maybe the manual should also make explicit that there is no aliasing between 
the Initialization and Rawness annotations - each checker only looks at their 
own annotations.

Original comment by wdi...@gmail.com on 2 May 2014 at 2:54

[GoogleCodeExporter]

[deleted comment]

[GoogleCodeExporter]

Sorry. I totally missed NullnessRawnessChecker. I thought like 
@UnderInitialization, @Raw is also checked by NullnessChecker. The manual 
mentions NullnessRawnessChecker but it may be nice to have a section to explain 
the difference between the rawness and initialization checkers. The manual 
says: "The rawness type system is slightly easier to use but slightly less 
expressive. In practice, you can use whichever one you prefer." Does the 
manually explain the differences between rawness and initialization in more 
depth? I haven't studied that part of the manual carefully. It's possible that 
the differences are already discussed somewhere in the manual and I just missed 
it.

Original comment by reprogra...@gmail.com on 2 May 2014 at 3:35

[GoogleCodeExporter]

The manual does not explicitly compare the two; rather, it describes each one 
independently.

The manual does note that one uses annotations @Initialized, 
@UnknownInitialization, and @UnderInitialization whereas the other uses 
annotations @Raw and @NonRaw.

I have added a note to the manual explaining that the main one (described 
throughout section 3.8) is preferred.  That will be pushed to the repository 
shortly.

Thanks for raising this issue!

Original comment by michael.ernst@gmail.com on 2 May 2014 at 4:03

• Changed state: Pushed

[GoogleCodeExporter]

Original comment by jtha...@cs.washington.edu on 3 Jun 2014 at 12:48

• Changed state: Fixed