package org.checkerframework.checker.lock.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.SubtypeOf;
import org.checkerframework.framework.qual.TargetLocations;
import org.checkerframework.framework.qual.TypeUseLocation;

/**
 * If a variable {@code x} has type {@code @GuardSatisfied}, then all lock expressions for {@code
 * x}'s value are held.
 *
 * <p>Written on a formal parameter (including the receiver), this annotation indicates that the
 * {@literal @}{@link GuardedBy} type for the corresponding actual argument at the method call site
 * is unknown at the method definition site, but any lock expressions that guard it are known to be
 * held prior to the method call.
 *
 * <p>For example, the formal parameter of the String copy constructor, {@link String#String(String
 * s)}, is annotated with {@code @GuardSatisfied}. This requires that all locks guarding the actual
 * argument are held when the constructor is called. However, the definition of the constructor does
 * not need to know what those locks are (and it cannot know, because the constructor can be called
 * by arbitrary code).
 *
 * @see GuardedBy
 * @see Holding
 * @checker_framework.manual #lock-checker Lock Checker
 * @checker_framework.manual #lock-checker-polymorphism-example Lock Checker polymorphism example
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.TYPE_USE)
@TargetLocations({TypeUseLocation.RECEIVER, TypeUseLocation.PARAMETER, TypeUseLocation.RETURN})
@SubtypeOf(GuardedByUnknown.class) // TODO: Should @GuardSatisfied be in its own hierarchy?
public @interface GuardSatisfied {
  /**
   * The index on the GuardSatisfied polymorphic qualifier. Defaults to -1 so that the user can
   * write any index starting from 0.
   */
  int value() default -1;
}