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.dataflow.qual.Pure;
import org.checkerframework.dataflow.qual.SideEffectFree;
import org.checkerframework.framework.qual.InheritedAnnotation;

/**
 * The method maintains a strictly nondecreasing lock held count on the current thread for any locks
 * that were held prior to the method call. The same property must in general be true of all the
 * methods it calls, which should themselves be annotated as {@code @ReleasesNoLocks} or a stronger
 * annotation such as {@code @}{@link SideEffectFree}.
 *
 * <p>The method might acquire locks but then release them, or might acquire locks but not release
 * them (in which case it should also be annotated with {@literal @}{@link EnsuresLockHeld} or
 * {@literal @}{@link EnsuresLockHeldIf}).
 *
 * <p>This is the default for methods being type-checked that have no {@code @}{@link LockingFree},
 * {@code @}{@link MayReleaseLocks}, {@code @}{@link SideEffectFree}, or {@code @}{@link Pure}
 * annotation.
 *
 * <p>{@code @ReleasesNoLocks} provides a guarantee unlike {@code @}{@link MayReleaseLocks}, which
 * provides no guarantees. However, {@code @ReleasesNoLocks} provides a weaker guarantee than
 * {@code @}{@link LockingFree}.
 *
 * @see MayReleaseLocks
 * @see LockingFree
 * @see SideEffectFree
 * @see Pure
 * @checker_framework.manual #lock-checker Lock Checker
 * @checker_framework.manual #lock-lockingfree-example Example use of @ReleasesNoLocks
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
@InheritedAnnotation
public @interface ReleasesNoLocks {}