False positive in the resource leak checker when the finalizer method has multiple @EnsuresCalledMethods annotation

[Nargeshdb]

Consider the following example, in which there's a class that includes two fields with non-empty must-call obligations. The resource leak checker is unable to verify that both fields are properly released in the finalizer method.

import org.checkerframework.checker.mustcall.qual.*;
import org.checkerframework.checker.calledmethods.qual.*;

class MultipleECMAnnosOnMethods {

  @InheritableMustCall("a")
  static class Foo {
    void a() {}
  }

  @InheritableMustCall("b")
  static class Bar {
    void b() {}
  }

  @InheritableMustCall("finalizer")
  static class OwningField {

    // :: warning: (required.method.not.called)
    private final @Owning Foo owningFoo;

    // :: warning: (required.method.not.called)
    private final @Owning Bar owningBar;

    public OwningField() {
      this.owningFoo = new Foo();
      this.owningBar = new Bar();
    }

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

  }
}

[jacek-lewandowski]

Shouldn't it be written like:

@EnsureCalledMethods.List({
    @EnsuresCalledMethods(value = {"this.owningBar"}, methods = {"b"})
    @EnsuresCalledMethods(value = {"this.owningFoo"}, methods = {"a"})
}

?

[msridhar]

Shouldn't it be written like:

@EnsureCalledMethods.List({
    @EnsuresCalledMethods(value = {"this.owningBar"}, methods = {"b"})
    @EnsuresCalledMethods(value = {"this.owningFoo"}, methods = {"a"})
}

?

@jacek-lewandowski since the @EnsuresCalledMethod annotation has a @Repeatable meta-annotation I think either variant is equivalent.