org.checkerframework.framework.qual

Annotation Type QualifierArgument

@Documented
 @Retention(value=RUNTIME)
 @Target(value=METHOD)
public @interface QualifierArgument

An annotation to use on an element of a contract annotation to indicate that the element specifies the value of an argument of the qualifier. A contract annotation is an annotation declared with a PreconditionAnnotation, PostconditionAnnotation, or ConditionalPostconditionAnnotation meta-annotation. The meta-annotation specifies the qualifier taking the arguments.

For example, the following code declares a postcondition annotation for the MinLen qualifier, allowing to specify its value:

  @PostconditionAnnotation(qualifier = MinLen.class)
  @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 public  @interface EnsuresMinLen {
   String[] value();
    @QualifierArgument("value")
   int targetValue() default 0;
 

The value element holds the expressions to which the qualifier applies and targetValue holds the value for the value argument of MinLen.

See Also:

PostconditionAnnotation, ConditionalPostconditionAnnotation, PreconditionAnnotation

Optional Element Summary

Optional Elements

Modifier and Type	Optional Element and Description
String	value Specifies the name of the argument of the qualifier, that is passed the values held in the annotated element.

Element Detail

value

public abstract String value

Specifies the name of the argument of the qualifier, that is passed the values held in the annotated element. If the value is omitted or is empty, then the name of the annotated element is used as the argument name.

Default:

""