Lock invariant violation reported too broadly on synchronized methods

[JLedelay]

When you fail to re-establish the lock invariant upon exiting a synchronized method, the entire class is reported as the origin for the error.
The following input:

public /*@ lock_invariant Perm(field, write); @*/ class C {
  int field;

  /*@
    requires committed(this);
  @*/
  public synchronized void inc() {
    loseWritePerm();
  }

  //@ requires Perm(field, write);
  public int loseWritePerm();
}

Generates the following output:

======================================
 At dbutils\lock\Test.java:1:1:
--------------------------------------
      [------------------------------------------------------------
    1  public /*@ lock_invariant Perm(field, write); @*/ class C {
    2    int field;
    3
       ... (7 lines omitted)
   11    //@ requires Perm(field, write);
   12    public int loseWritePerms();
   13  }
       -]
   14
--------------------------------------
[1/2] The lock invariant may not be exhaled here, since ...
--------------------------------------
 At dbutils\lock\Test.java:1:27:
--------------------------------------
                                [------------------
    1  public /*@ lock_invariant Perm(field, write); @*/ class C {
                                 ------------------]
    2    int field;
    3
--------------------------------------
[2/2] ... there might not be enough permission to exhale this amount (https://utwente.nl/vercors#invariantFailed:perm)
======================================

This ought to report the method instead, similarly to how a synchronized block is highlighted when it fails to re-establish the lock invariant.