| package org.checkerframework.dataflow.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; |
| |
| /** |
| * A method is called <em>side-effect-free</em> if it has no visible |
| * side-effects, such as setting a field of an object that existed before |
| * the method was called. |
| * <p> |
| * Only the visible side-effects are important. The method is allowed to cache |
| * the answer to a computationally expensive query, for instance. It is also |
| * allowed to modify newly-created objects, and a constructor is |
| * side-effect-free if it does not modify any objects that existed before |
| * it was called. |
| * <p> |
| * This annotation is important to pluggable type-checking because if some |
| * fact about an object is known before a call to such a method, then the |
| * fact is still known afterwards, even if the fact is about some non-final |
| * field. When any non-{@code @SideEffectFree} method is called, then a |
| * pluggable type-checker must assume that any field of any accessible |
| * object might have been modified, which annuls the effect of |
| * flow-sensitive type refinement and prevents the pluggable type-checker |
| * from making conclusions that are obvious to a programmer. |
| * <p> |
| * Also see {@link Pure}, which means both side-effect-free and {@link |
| * Deterministic}. |
| * <p> |
| * <b>Analysis:</b> |
| * The Checker Framework performs a conservative analysis to verify a |
| * {@code @SideEffectFree} annotation. |
| * The Checker Framework issues a warning |
| * if the method uses any of the following Java constructs: |
| * <ol> |
| * <li>Assignment to any expression, except for local variables and method |
| * parameters. |
| * <li>A method invocation of a method that is not {@code @SideEffectFree}. |
| * <li>Construction of a new object where the constructor is not {@code @SideEffectFree}. |
| * </ol> |
| * These rules are conservative: any code that passes the checks is |
| * side-effect-free, but the Checker Framework may issue false positive |
| * warnings, for code that uses one of the forbidden constructs but is |
| * side-effect-free nonetheless. In particular, a method that caches its |
| * result will be rejected. |
| * <p> |
| * |
| * In fact, the rules are so conservative that checking is currently |
| * disabled by default, but can be enabled via the |
| * {@code -AcheckPurityAnnotations} command-line option. |
| * <p> |
| * |
| * @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and flow-sensitive analysis |
| * |
| * @author Stefan Heule |
| */ |
| @Documented |
| @Retention(RetentionPolicy.RUNTIME) |
| @Target({ ElementType.METHOD, ElementType.CONSTRUCTOR }) |
| public @interface SideEffectFree { |
| } |