Example of @UnderInitialization in manual is incorrect

[GoogleCodeExporter]

What steps will reproduce the problem?
Run the nullness checker on the following code:

import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.initialization.qual.*;

public class TreeNode {
  Object data;
  TreeNode left;
  TreeNode right;

  public TreeNode(Object data, TreeNode l, TreeNode r) {
    this.data = data;
    setChildren(l, r);
  }

  @EnsuresNonNull({"left", "right"})
  void setChildren(@UnderInitialization(TreeNode.class) TreeNode this, TreeNode l, TreeNode r) {
    left = l;
    right = r;
  }

}

What is the expected output? What do you see instead?
I expect no warnings. Instead, the checker reports the warning below:

rc/TreeNode.java:11: warning: [method.invocation.invalid] call to 
setChildren(TreeNode,TreeNode) not allowed on the given receiver.
    this.setChildren(l, r);
                    ^
  found   : @UnderInitialization(java.lang.Object.class) @NonNull TreeNode
  required: @UnderInitialization(TreeNode.class) @NonNull TreeNode
1 warning

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

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

[GoogleCodeExporter]

Hi Mohsen,

this is the correct behavior.
The argument to @UnderInitialization is inclusive.
At the call to setChildren, the TreeNode object is not fully initialized - the 
left and right fields are not set yet.
Your signature for setChildren requires that at least the TreeNode fields are 
initialized - which is not the case at the call site - and the correct error is 
raised.

To make the example pass, you simply need to change the signature to:

  @EnsuresNonNull({"left", "right"})
  void setChildren(@UnderInitialization(Object.class) TreeNode this, TreeNode l, TreeNode r) {

Does this behavior make sense now?
Is there documentation that we're missing? The Javadoc at

https://code.google.com/p/checker-framework/source/browse/checker/src/org/checke
rframework/checker/initialization/qual/UnderInitialization.java

highlights that the argument is inclusive multiple times.

Thanks,
cu, WMD.

Original comment by wdi...@gmail.com on 1 May 2014 at 4:33

• Changed state: Invalid

[GoogleCodeExporter]

Hi Werner,

Thank you for your quick response. I noticed that the javadoc mentioned 
"inclusive" and wondered if it's a bug in the manual, javadoc, or the checker. 
Your response implies that the bug is in the manual. See the example code for 
@UnderInitialization at 
<http://types.cs.washington.edu/checker-framework/current/checkers-manual.html#i
nitialization-checker>. Per your explanation, I expect the checker to raise an 
error on the code example in the manual, right?

Original comment by reprogra...@gmail.com on 1 May 2014 at 4:52

[GoogleCodeExporter]

I agree that the second "MyClass" example in the Initialization Checker manual 
seems wrong.
I think it would be best to have MyClass and MySuperClass and to detail how the 
two different frames are related.

cu, WMD.

Original comment by wdi...@gmail.com on 1 May 2014 at 6:16

• Changed title: Example of @UnderInitialization in manual is incorrect
• Changed state: Accepted

[GoogleCodeExporter]

Fix together with Issue 327.

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

• Added labels: Manual