Fix unsoundess in Resource Leak Checker related to owning fields and EnsuresCalledMethods

[kelloggm]

Fixes #4838.

Merge after #4867.

This is a replacement for #4839, based on the comments on it from @msridhar. It relies on #4867 to resolve the false positives described in the comment chain on #4839.

[msridhar]

This looks pretty clean! The change looks good to me. Do we have a test where the finalizer does a try-finally and we are able to still verify it?

[kelloggm]

Do we have a test where the finalizer does a try-finally and we are able to still verify it?

We did not, but I just added one as ReplicaInputStreams2.java.

[msridhar]

Mostly LGTM; just one style comment

[msridhar]

Sorry, one more question I forgot to ask before

[msridhar]

Why are we adding these exception types in this PR? Do the tests not pass without it?

[kelloggm]

The tests do not pass without it.

In particular, we get these three false positives:

    3 unexpected diagnostics were found
    CheckFields.java:68: error: (destructor.exceptional.postcondition)
    CreatesMustCallForOverride2.java:38: error: (destructor.exceptional.postcondition)
    CreatesMustCallForOverride2.java:56: error: (destructor.exceptional.postcondition)

For reference, here's the relevant lines of CheckFields:

    @EnsuresCalledMethods(
        value = {"this.finalOwningFoo", "this.owningFoo"},
        methods = {"a"})
    void b() {
      this.finalOwningFoo.a();
      this.finalOwningFoo.c();
      this.owningFoo.a();
    }
  }

[msridhar]

After this lands we may want to think about another manual update like #4892

[kelloggm]

I'm not sure that's really necessary - that run-time errors don't invalidate CalledMethods types follows from the idea that annotations (and therefore types) specify normal behavior, and a run-time exception is definitely not normal behavior.