EnsuresQualifier (checker-framework 3.39.0-eisop1 API)

```
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@InheritedAnnotation
@Repeatable(List.class)
public @interface EnsuresQualifier
```
A postcondition annotation to indicate that a method ensures that certain expressions have a certain type qualifier once the method has successfully terminated. The expressions for which the qualifier holds after the method's execution are indicated by expression and are specified using a string. The qualifier is specified by the qualifier annotation element.
Here is an example use:
```
  @EnsuresQualifier(expression = "p.f1", qualifier = Odd.class)
   void oddF1_1() {
       p.f1 = null;
   }
 
```
Some type systems have specialized versions of this annotation, such as org.checkerframework.checker.nullness.qual.EnsuresNonNull and org.checkerframework.checker.lock.qual.EnsuresLockHeld.
See Also:

EnsuresQualifierIf

See the Checker Framework Manual:
Syntax of Java expressions

Required Element Summary

Required Elements
Modifier and Type	Required Element	Description
`java.lang.String[]`	`expression`	Returns the Java expressions for which the qualifier holds after successful method termination.
`java.lang.Class<? extends java.lang.annotation.Annotation>`	`qualifier`	Returns the qualifier that is guaranteed to hold on successful termination of the method.

- Element Detail
  - expression
```
java.lang.String[] expression
```
    Returns the Java expressions for which the qualifier holds after successful method termination.
    
    Returns:
    
    the Java expressions for which the qualifier holds after successful method termination
    
    See the Checker Framework Manual:
    Syntax of Java expressions
- - qualifier
```
java.lang.Class<? extends java.lang.annotation.Annotation> qualifier
```
    Returns the qualifier that is guaranteed to hold on successful termination of the method.
    
    Returns:
    
    the qualifier that is guaranteed to hold on successful termination of the method