Poor error messages for `@EnsuresCalledMethods`

[Calvin-L]

The Resource Leak Checker provides clear error messages for resources allocated in a method:

    void m1() throws IOException {
        Closeable resource = alloc();
        doSomething();
        resource.close();
    }

ErrorMessagesForEnsuresCalledMethods.java:[16,18] error: [required.method.not.called] @MustCall method close may not have been invoked on resource or any of its aliases.
  The type of object is: java.io.Closeable.
  Reason for going out of scope: possible exceptional exit due to doSomething() with exception type java.io.IOException

But its error messages for very similar code using @EnsuresCalledMethods and/or @EnsuresCalledMethodsOnException are not nearly as helpful:

    @EnsuresCalledMethods(value="#1", methods="close")
    @EnsuresCalledMethodsOnException(value="#1", methods="close")
    void m2(Closeable resource) throws IOException {
        doSomething();
        resource.close();
    }

ErrorMessagesForEnsuresCalledMethods.java:[23,9] error: [contracts.exceptional.postcondition] on exception, postcondition of m2 is not satisfied.
  found   : #1 is @CalledMethods
  required: #1 is @CalledMethods("close")

Side-by-side it's clear that the bug in m2 is the same as the bug in m1, but in practice it's rarely clear what contributes to the error. Ideally the error message for m2 would include something similar to the first error, e.g.

  Behavior leading to this condition: exceptional exit when doSomething() throws java.io.IOException

(I know just enough about the Checker Framework to suspect that this will be difficult to fix---but I think it would be a big step up if possible.)

[msridhar]

I'm not 100% sure why this would be hard to fix. Do we account for resource aliases when checking @EnsuresCalledMethodsOnException? If so, we should already be running the analysis that computes the more detailed info, and maybe we could hack the error message based on that.

[Calvin-L]

I believe the postcondition annotations are handled by framework scaffolding, where the obligation information tracked by MustCallConsistencyAnalyzer is not available. (But it's been a while since I looked at that code, so I might be misremembering.)