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
Original issue reported on code.google.com by
michael.ernst@gmail.com
on 30 Oct 2012 at 1:21