Poor error messages for `@EnsuresCalledMethods`

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.)

Start with ErrorMessagesForEnsuresCalledMethods.java and the diagnostics for @EnsuresCalledMethods and @EnsuresCalledMethodsOnException. Trace how exceptional postcondition failures are reported, then add context identifying the exceptional exit and verify the resulting message against the m2 example.