Resource initialization after a `super()` call should be permitted.

[mernst]

Consider the following code, which is checked in as InitializationAfterSuperTest.java:

import java.io.IOException;
import java.net.Socket;
import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
import org.checkerframework.checker.mustcall.qual.InheritableMustCall;
import org.checkerframework.checker.mustcall.qual.Owning;

@InheritableMustCall("close")
public class InitializationAfterSuperTest implements AutoCloseable {

  @Owning Socket mySocket;

  public InitializationAfterSuperTest(@Owning Socket mySocket) {
    super();
    this.mySocket = mySocket;
  }

  @EnsuresCalledMethods(value = "mySocket", methods = "close")
  @Override
  public void close() throws IOException {
    mySocket.close();
  }
}

The Resource Leak Checker issues this error:

InitializationAfterSuperTest.java:14: error: [required.method.not.called] @MustCall method close may not have been invoked on field mySocket or any of its aliases.
    this.mySocket = mySocket;
                  ^
  The type of object is: java.net.Socket.
  Reason for going out of scope:  Non-final owning field might be overwritten

Initialization after a super() call is a common pattern and the checker should permit it, at least by default. (There could be a flag to make the checker issue a warning, on the off chance that super() made a call that assigned mySocket.)

[kelloggm]

(There could be a flag to make the checker issue a warning, on the off chance that super() made a call that assigned mySocket.)

While this may be common enough to warrant introducing an unsoundness into the checker, I think we need to be clear that that would be what we're doing here. I'm not sure I'm comfortable making that the default behavior: it is possible that this.mySocket does contain a resource at the point where the warning is issued.

A programmer could avoid the problem by e.g., doing a null check on this.mySocket before the assignment. For example, the RLC currently verifies the below code, which I'd argue is safer:

@InheritableMustCall("close")
public class InitializationAfterSuperTest implements AutoCloseable {

  @Owning Socket mySocket;

  public InitializationAfterSuperTest(@Owning Socket mySocket) throws IOException {
    super();
    if (this.mySocket == null) {
      this.mySocket = mySocket;
    } else {
      mySocket.close();
    }
  }

  @EnsuresCalledMethods(value = "mySocket", methods = "close")
  @Override
  public void close() throws IOException {
    mySocket.close();
  }
}

This code solves the problem: if the super() call does put a resource in this.mySocket, all resources are still accounted for. While I agree with you that code like the example in your test case is common, I'm not sure that we should be encouraging programmers to write it, because it is technically unsafe.

[mernst]

I would be OK with defaulting to sound behavior and adding a flag to permit initialization after a super() call. It would be useful when annotating legacy codebases.