It should be possible to assign non-final, owning fields in constructors safely

[kelloggm]

Our analysis cannot verify simple container classes like SocketContainer.java (below), because it assumes that any non-final, owning field might already have a value. This is a problem, because at some point every field has to be assigned for the first time! We can only ever verify that first assignment now if it is (a) guarded by a null checker, or (b) in the initializer. For example, we cannot verify:

@MustCall("close")
class SocketContainer {
    @Owning Socket sock;

    public SocketContainer(String host, int port) throws Exception {
        // Warning here, because sock might be overwritten.
        sock = new Socket(host, port);
    }

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

The reason is that sock might be overwritten when it is assigned in the constructor. In this particular case, we can tell that's not true (i.e. this is a false positive).

Here is a (possibly incomplete) list of ways that a non-final, owning field might be assigned before an assignment in a constructor that we would like to verify:

1. it might have an initializer that assigns it to a non-null value
2. it might be assigned by a superclass constructor (i.e. a super() call)
3. it might be assigned by a different constructor (i.e. a this() call)
4. it might be assigned earlier in the same constructor
5. it might be assigned by some method that the constructor calls
6. it might be assigned in an initializer block

In order to verify an arbitrary assignment in a constructor, we'd have to check all of these (and make sure the list is complete!).

It might be possible to use the Initialized Fields Checker to help with this problem. I don't think we could just use its analysis directly, since it's proving the opposite of what we're interested in - we want to show that a field is definitely NOT initialized at the point where it is assigned.