Annotation Interface DoesNotUnrefineReceiver


@Documented @InheritedAnnotation @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) public @interface DoesNotUnrefineReceiver
At a call to a side-effecting method, the framework ordinarily discards all refined type information, since the side-effecting method might invalidate that information. This annotation indicates that, at a call to the annotated method, the receiver's type should not be unrefined. That is, a call to the method does not affect the type qualifier (in the given hierarchy).
See the Checker Framework Manual:
Side effects, determinism, purity, and flow-sensitive analysis
  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    The name of the checker(s) that this annotation affects.
  • Element Details

    • value

      String[] value
      The name of the checker(s) that this annotation affects. For example, "modifiability" or "nullness". Use "allcheckers" to affect all checkers.
      Returns:
      the name of the checker that this annotation affects