Why we need to add @EnsuresCalledMethods for resource.close even if resource.close is the only call in the method?

[jacek-lewandowski]

Unless close is explicitly annotated with @EnsuresCalledMethods("this.resource", "close"), the analyser complains with required.method.not.called on the resource declaration.

    @Owning InputStream resource;

    public void close()
    {
        resources.close();
    }

Is it a bug or expected behaviour?

[kelloggm]

Is it a bug or expected behaviour?

This is expected behavior. The analysis is modular, meaning that it only analyzes each program element once. When analyzing element A (in this case, the field resource), the analysis is therefore only able to use the signature of some other element B (in this case, the method close()): it is not able to introspect into close() to see that it calls resources.close(). The @EnsuresCalledMethods annotation makes this information visible outside the method.