Add @RequiresPresent annotation

checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethodsIf.java

@@ -25,6 +25,13 @@
 @InheritedAnnotation
 @Repeatable(EnsuresCalledMethodsIf.List.class)
 public @interface EnsuresCalledMethodsIf {
+  /**
+   * Returns the return value of the method under which the postcondition holds.
+   *
+   * @return the return value of the method under which the postcondition holds
+   */
+  boolean result();
+
   /**
    * Returns Java expressions that have had the given methods called on them after the method
    * returns {@link #result}.
@@ -34,13 +41,6 @@
    */
   String[] expression();
 
-  /**
-   * Returns the return value of the method under which the postcondition holds.
-   *
-   * @return the return value of the method under which the postcondition holds
-   */
-  boolean result();
-
   /**
    * The methods guaranteed to be invoked on the expressions if the result of the method is {@link
    * #result}.

checker-qual/src/main/java/org/checkerframework/checker/index/qual/EnsuresLTLengthOfIf.java

@@ -58,17 +58,23 @@
 @InheritedAnnotation
 @Repeatable(EnsuresLTLengthOfIf.List.class)
 public @interface EnsuresLTLengthOfIf {
+  /**
+   * The return value of the method that needs to hold for the postcondition to hold.
+   *
+   * @return the return value of the method that needs to hold for the postcondition to hold
+   */
+  boolean result();
+
   /**
    * Java expression(s) that are less than the length of the given sequences after the method
    * returns the given result.
    *
+   * @return Java expression(s) that are less than the length of the given sequences after the
+   *     method returns the given result
    * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
    */
   String[] expression();
 
-  /** The return value of the method that needs to hold for the postcondition to hold. */
-  boolean result();
-
   /**
    * Sequences, each of which is longer than each of the expressions' value after the method returns
    * the given result.

checker-qual/src/main/java/org/checkerframework/checker/lock/qual/EnsuresLockHeldIf.java

@@ -24,6 +24,13 @@
 @InheritedAnnotation
 @Repeatable(EnsuresLockHeldIf.List.class)
 public @interface EnsuresLockHeldIf {
+  /**
+   * Returns the return value of the method under which the postconditions hold.
+   *
+   * @return the return value of the method under which the postconditions hold
+   */
+  boolean result();
+
   /**
    * Returns Java expressions whose values are locks that are held after the method returns the
    * given result.
@@ -38,13 +45,6 @@
   // assumes that conditional postconditions have a field named "expression".
   String[] expression();
 
-  /**
-   * Returns the return value of the method under which the postconditions hold.
-   *
-   * @return the return value of the method under which the postconditions hold
-   */
-  boolean result();
-
   /**
    * A wrapper annotation that makes the {@link EnsuresLockHeldIf} annotation repeatable.
    *

checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/EnsuresNonNullIf.java

@@ -46,8 +46,7 @@
  *   }}</pre>
  *
  * An {@code EnsuresNonNullIf} annotation that refers to a private field is useful for verifying
- * that client code performs needed checks in the right order, even if the client code cannot
- * directly affect the field.
+ * that a method establishes a property, even though client code cannot directly affect the field.
  *
  * <p><b>Method calls:</b> If {@link Class#isArray()} returns true, then {@link
  * Class#getComponentType()} returns non-null. You can express this relationship as:
@@ -76,19 +75,19 @@
 @Repeatable(EnsuresNonNullIf.List.class)
 public @interface EnsuresNonNullIf {
   /**
-   * Returns Java expression(s) that are non-null after the method returns the given result.
+   * Returns the return value of the method under which the postcondition holds.
    *
-   * @return Java expression(s) that are non-null after the method returns the given result
-   * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
+   * @return the return value of the method under which the postcondition holds
    */
-  String[] expression();
+  boolean result();
 
   /**
-   * Returns the return value of the method under which the postcondition holds.
+   * Returns Java expression(s) that are non-null after the method returns the given result.
    *
-   * @return the return value of the method under which the postcondition holds
+   * @return Java expression(s) that are non-null after the method returns the given result
+   * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
    */
-  boolean result();
+  String[] expression();
 
   /**
    * * A wrapper annotation that makes the {@link EnsuresNonNullIf} annotation repeatable.

checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/RequiresNonNull.java

@@ -55,7 +55,7 @@
  *
  * Do not use this annotation for formal parameters (instead, give them a {@code @NonNull} type,
  * which is the default and need not be written). The {@code @RequiresNonNull} annotation is
- * intended for other expressions, such as field accesses or method calls.
+ * intended for non-parameter, such as field accesses or method calls.
  *
  * @checker_framework.manual #nullness-checker Nullness Checker
  */

checker-qual/src/main/java/org/checkerframework/checker/optional/qual/EnsuresPresentIf.java

@@ -10,7 +10,7 @@
 
 /**
  * Indicates that the given expressions of type Optional<T> are present, if the method returns
- * the given result (either true or false).FOO
+ * the given result (either true or false).
  *
  * <p>Here are ways this conditional postcondition annotation can be used:
  *
@@ -25,23 +25,22 @@
  *
  * because, if {@code isPresentAndEqual} returns true, then the first (#1) argument to {@code
  * isPresentAndEqual} was present, and so was the second (#2) argument. Note that you can write two
- * {@code @EnsurePresentIf} annotations on a single method.
+ * {@code @EnsuresPresentIf} annotations on a single method.
  *
  * <p><b>Fields:</b> The value expressions can refer to fields, even private ones. For example:
  *
  * <pre><code> &nbsp;@EnsuresPresentIf(expression="this.optShape", result=true)
  *  public boolean isShape() {
  *    return (this.optShape != null &amp;&amp; this.optShape.isPresent());
- * }</code></pre>
+ *  }</code></pre>
  *
  * An {@code @EnsuresPresentIf} annotation that refers to a private field is useful for verifying
- * that client code performs needed checks in the right order, even if the client code cannot
- * directly affect the field.
+ * that a method establishes a property, even though client code cannot directly affect the field.
  *
  * <p><b>Method postconditions:</b> Suppose that if a method {@code isRectangle()} returns true,
  * then {@code getRectangle()} will return a present Optional. You an express this relationship as:
  *
- * <pre>{@code @EnsuresPresentIf(result=true, expression="getRectangle()")
+ * <pre>{@code  @EnsuresPresentIf(result=true, expression="getRectangle()")
  * public @Pure isRectangle() { ... }}</pre>
  *
  * @see Present
@@ -54,23 +53,23 @@
 @ConditionalPostconditionAnnotation(qualifier = Present.class)
 @InheritedAnnotation
 public @interface EnsuresPresentIf {
+  /**
+   * Returns the return value of the method under which the postcondition holds.
+   *
+   * @return the return value of the method under which the postcondition holds
+   */
+  boolean result();
+
   /**
    * Returns the Java expressions of type Optional&lt;T&gt; that are present after the method
    * returns the given result.
    *
    * @return the Java expressions of type Optional&lt;T&gt; that are present after the method
-   *     returns the given result. value {@link #result()}
+   *     returns the given result.
    * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
    */
   String[] expression();
 
-  /**
-   * Returns the return value of the method under which the postcondition holds.
-   *
-   * @return the return value of the method under which the postcondition holds.
-   */
-  boolean result();
-
   /**
    * A wrapper annotation that makes the {@link EnsuresPresentIf} annotation repeatable.
    *
@@ -84,7 +83,7 @@
     /**
      * Returns the repeatable annotations.
      *
-     * @return the repeatable annotations.
+     * @return the repeatable annotations
      */
     EnsuresPresentIf[] value();
   }

checker-qual/src/main/java/org/checkerframework/checker/optional/qual/RequiresPresent.java

@@ -0,0 +1,90 @@
+package org.checkerframework.checker.optional.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.PreconditionAnnotation;
+
+/**
+ * Indicates a method precondition: the specified expressions of type Optional must be present
+ * (i.e., non-empty) when the annotated method is invoked.
+ *
+ * <p>For example:
+ *
+ * <pre>
+ * import java.util.Optional;
+ *
+ * import org.checkerframework.checker.optional.qual.RequiresPresent;
+ * import org.checkerframework.checker.optional.qual.Present;
+ *
+ * class MyClass {
+ *   Optional&lt;String&gt; optId1;
+ *   Optional&lt;String&gt; optId2;
+ *
+ * &nbsp; @RequiresPresent({"optId1", "#1.optId1"})
+ *   void method1(MyClass other) {
+ *     optId1.get().length()       // OK, this.optID1 is known to be present.
+ *     optId2.get().length()       // error, might throw NoSuchElementException.
+ *
+ *     other.optId1.get().length() // OK, this.optID1 is known to be present.
+ *     other.optId2.get().length() // error, might throw NoSuchElementException.
+ *   }
+ *
+ *   void method2() {
+ *     MyClass other = new MyClass();
+ *
+ *     optId1 = Optional.of("abc");
+ *     other.optId1 = Optional.of("def")
+ *     method1(other);                       // OK, satisfies method precondition.
+ *
+ *     optId1 = Optional.empty();
+ *     other.optId1 = Optional.empty("abc");
+ *     method1(other);                       // error, does not satisfy this.optId1 method precondition.
+ *
+ *     optId1 = Optional.empty("abc");
+ *     other.optId1 = Optional.empty();
+ *     method1(other);                       // error. does not satisfy other.optId1 method precondition.
+ *   }
+ * }
+ * </pre>
+ *
+ * Do not use this annotation for formal parameters (instead, give them a {@code @Present} type).
+ * The {@code @RequiresNonNull} annotation is intended for non-parameter expressions, such as field
+ * accesses or method calls.
+ *
+ * @checker_framework.manual #optional-checker Optional Checker
+ */
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+@PreconditionAnnotation(qualifier = Present.class)
+public @interface RequiresPresent {
+
+  /**
+   * The Java expressions that that need to be {@link Present}.
+   *
+   * @return the Java expressions that need to be {@link Present}
+   * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
+   */
+  String[] value();
+
+  /**
+   * A wrapper annotation that makes the {@link RequiresPresent} annotation repeatable.
+   *
+   * <p>Programmers generally do not need to write this. It is created by Java when a programmer
+   * writes more than one {@link RequiresPresent} annotation at the same location.
+   */
+  @Documented
+  @Retention(RetentionPolicy.RUNTIME)
+  @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+  @PreconditionAnnotation(qualifier = Present.class)
+  public static @interface List {
+    /**
+     * Returns the repeatable annotations.
+     *
+     * @return the repeatable annotations
+     */
+    RequiresPresent[] value();
+  }
+}

checker-qual/src/main/java/org/checkerframework/common/value/qual/EnsuresMinLenIf.java

@@ -27,6 +27,13 @@
 @InheritedAnnotation
 @Repeatable(EnsuresMinLenIf.List.class)
 public @interface EnsuresMinLenIf {
+  /**
+   * Returns the return value of the method under which the postcondition to hold.
+   *
+   * @return the return value of the method under which the postcondition to hold
+   */
+  boolean result();
+
   /**
    * Returns Java expression(s) that are a sequence with the given minimum length after the method
    * returns {@link #result}.
@@ -37,13 +44,6 @@
    */
   String[] expression();
 
-  /**
-   * Returns the return value of the method under which the postcondition to hold.
-   *
-   * @return the return value of the method under which the postcondition to hold
-   */
-  boolean result();
-
   /**
    * Returns the minimum number of elements in the sequence.
    *

checker-qual/src/main/java/org/checkerframework/framework/qual/EnsuresQualifierIf.java

@@ -39,6 +39,13 @@
 @InheritedAnnotation
 @Repeatable(EnsuresQualifierIf.List.class)
 public @interface EnsuresQualifierIf {
+  /**
+   * Returns the return value of the method that needs to hold for the postcondition to hold.
+   *
+   * @return the return value of the method that needs to hold for the postcondition to hold
+   */
+  boolean result();
+
   /**
    * Returns the Java expressions for which the qualifier holds if the method terminates with return
    * value {@link #result()}.
@@ -58,13 +65,6 @@
    */
   Class<? extends Annotation> qualifier();
 
-  /**
-   * Returns the return value of the method that needs to hold for the postcondition to hold.
-   *
-   * @return the return value of the method that needs to hold for the postcondition to hold
-   */
-  boolean result();
-
   /**
    * A wrapper annotation that makes the {@link EnsuresQualifierIf} annotation repeatable.
    *

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java

@@ -681,7 +681,7 @@ private void computeOwningFromInvocation(Set<Obligation> obligations, Node invoc
    *
    * @param invocation the MethodInvocationNode
    * @param varJe a Java expression
-   * @return the called methods annotation for the {@code varJe} after the {@code invocation} node.
+   * @return the called methods annotation for the {@code varJe} after the {@code invocation} node
    */
   private AnnotationMirror getCalledMethodsAnno(
       MethodInvocationNode invocation, JavaExpression varJe) {

checker/tests/calledmethods/Postconditions.java

@@ -1,6 +1,6 @@
 import org.checkerframework.checker.calledmethods.qual.*;
 
-/** Test for postcondition support via @EnsureCalledMethods. */
+/** Test for postcondition support via @EnsuresCalledMethods. */
 public class Postconditions {
   void build(@CalledMethods({"a", "b", "c"}) Postconditions this) {}