ThrowsExceptionTest: ExceptionUsages.doesNotThrowException() is falsely annotated

[Michael Reif]

@DoesNotThrowException(
            reason="just returns constant",
            requires={}
    )
    public int doesNotThrowException() {
        return 2;
    }

This method is falsely annotated. The method is public, non-final, and located in the public class ExceptionUsages. Therefore, the method doesNotThrowException() is always overridable!! Moreover, this means that the method invocation might throws an exception. The only exception is when an application is analyzed and ExceptionUsage can be considered final.

I'm not sure if you can add this restriction to the annotations' requires clause.

[Andreas M]

The method itself is correctly annotated, because as for its own it doesn't throw an exception. If another method x calls doesNotThrowException, x may throw an exception because doesNotThrowException is overrideable and we may not know all implementations. I already fixed the tests in this PR.

[Michael Eichberg]

Closing this issue - the described issue is solved by using the aggregating analysis.