All inheritable declaration annotations are being inherited, regardless of their relationship

[GoogleCodeExporter]

When inheriting related declaration annotations, the element should inherit 
only the "stronger ones", instead of all of them.

For example:
class Super {
     @Pure 
     void foo(){}
}   

class clazz extends Super {
     @SideEffectFree
     @Override
     void foo(){}
}

We want clazz.foo() to have only the @Pure annotation since @Pure and 
@SideEffectFree are related, but instead it currently has both of them.

There is a test case for that issue in 
checker-framework/checker/jtreg/nullness/inheritDeclAnnoPersist/Extends.java: 
method m3().

Original issue reported on code.google.com by pbsf...@gmail.com on 17 Jul 2014 at 10:12

[GoogleCodeExporter]

With this issue we should also discuss when an error should be raised.
In the original example:

class Super {
     @Pure 
     void foo(){}
}   

class clazz extends Super {
     @SideEffectFree
     @Override
     void foo(){}
}

The overriding method uses a weaker purity annotation and an error would be 
appropriate, instead of silently changing the qualifier to @Pure in bytecode.

The opposite example:

class Super2 {
     @SideEffectFree
     void foo(){}
}   

class clazz2 extends Super {
     @Pure 
     @Override
     void foo(){}
}

should work and only store a single qualifier each, @SEF in Super2.foo and 
@Pure in clazz2.foo.

Original comment by wdi...@gmail.com on 18 Jul 2014 at 8:04

• Changed state: Accepted