search

biddyweb / checker-framework

Automatically exported from code.google.com/p/checker-framework
Other
0 stars 1 forks source link

Annotated JDK and unannotated methods that have an annotation in a superclass #371

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
As of this writing, the annotated JDK does not contain a URL.java file for the 
java.net.URL class.
Nonetheless, the following code should type-check.
This could be handled via inheritance of annotations from superclasses either 
during JDK creation or during type-checking.
It would be impractical to manually annotate every method in the entire JDK:  
it would be too labor-intensive and there would be certain to be some 
oversights.

I believe that the Checker Framework already does inherit annotations from 
superclasses , but I don't see documentation of this in the manual.  Rather, 
section 21.3.3, "Inherited defaults", argues against such a polity, and the end 
of 21.4.3 says, "In the future, the Checker Framework will support inheriting 
annotations from superclass definitions."

A test case appears at 
checker-framework/checker/tests/nullness/AnnotatedJdkEqualsTest.java

Original issue reported on code.google.com by michael.ernst@gmail.com on 30 Sep 2014 at 7:18