Possible dataflow bug

[GoogleCodeExporter]

In the following example, shouldn't 'result' definitely be initialized to a 
non-null Object before it is returned?

Perhaps the flow analysis is allowing for 'p' to be null? In that case p.get() 
would throw a NPE and 'result' wouldn't get initialized.

# Steps to reproduce

=== Test.java ===
class Test {
  interface Provider {
    Object get();
  }
  Object execute(Provider p) {
    final Object result;
    try {
      result = p.get();
    } finally {
    }
    return result;
  }
}
===

$ ~/jsr308/checker-framework-1.8.3/checker/bin/javac -processor 
org.checkerframework.checker.nullness.NullnessChecker -cp 
~/jsr308/checker-framework-1.8.3/checker/dist/checker-qual.jar Test.java
Test.java:13: error: [return.type.incompatible] incompatible types in return.
    return result;
           ^
  found   : @UnknownInitialization @Nullable Object
  required: @Initialized @NonNull Object
1 error

Original issue reported on code.google.com by cus...@google.com on 15 Jul 2014 at 11:37

[GoogleCodeExporter]

If the get() method throws an exception, then the assignment to p does not 
occur.
For that reason, the warning is correct.  (The warning isn't related to p nor 
the result of get being possibly null.)

If you have suggestions for how to make subtle issues like this clearer to 
users of the Checker Framework, that would be great.  Thanks!

Original comment by michael.ernst@gmail.com on 16 Jul 2014 at 12:01

• Changed state: Invalid

[GoogleCodeExporter]

If 'get' is a field, the same diagnostic is reported. Is there another place 
the assignment could fail?

e.g.

class Test {
  static class Provider {
    public final Object get = new Object();
  }
  Object execute(Provider p) {
    final Object result;
    try {
      result = p.get;
    } finally {
    }
    return result;
  }
}

Original comment by cus...@google.com on 16 Jul 2014 at 12:36

[GoogleCodeExporter]

This looks similar to Issue 293, but separate.
In the CFG, p.get might create a NPE (the CFG doesn't consider the Checker 
Framework types). Then after the merge "result" may be unitialized and nullable.

We need to prune paths based on the Checker Framework types. Because p is 
@NonNull, we know that p.get cannot throw an NPE. Therefore, we don't need to 
merge with that store.
Would that make sense?

Original comment by wdi...@gmail.com on 16 Jul 2014 at 2:34

• Changed state: Accepted

[GoogleCodeExporter]

Original comment by wdi...@gmail.com on 16 Jul 2014 at 2:35

• Added labels: Dataflow