barry-m / checker-framework

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

Aliasing a single third-party annotation to both a type qualifier and a declaration annotation #171

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
The book "Java Concurrency in Practice" defines a @GuardedBy annotation that 
serves two distinct purposes.  The Checker Framework uses two distinct 
annotations for the two purposes.  The JCIP annotation can be used on a field 
(in which case it is a type qualifier corresponding to the Lock Checker's 
@GuardedBy) or on a method (in which case it is a declaration annotation 
corresponding to the Lock Checker's @Holding).  Also see 
http://types.cs.washington.edu/checker-framework/current/checkers-manual.html#jc
ip-annotations

The need to rewrite some occurrences of @GuardedBy to @Holding may be 
inconvenient for users who wish to use the Lock Checker to type-check code that 
already contains JCIP annotations.  It would be useful if occurrences of the 
JCIP @GuardedBy that are written on methods were treated as @Holding, whereas 
occurrences of the JCIP @GuardedBy that are written on fields are treated as 
@GuardedBy.

This would probably require enhancements to the annotation-aliasing mechanism, 
or special-case code just for the Lock Checker.  Then, the behavior would need 
to be tested and documented in the manual.

Original issue reported on code.google.com by michael.ernst@gmail.com on 30 Oct 2012 at 1:21

GoogleCodeExporter commented 9 years ago

Original comment by Jonathan...@gmail.com on 15 Apr 2014 at 7:11