Package org.checkerframework.dataflow.qual

Annotation Interface SideEffectsOnly

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) public @interface SideEffectsOnly
A method annotated with the declaration annotation @SideEffectsOnly({"A", "B"}) changes the value of at most the expressions A and B. No other expression is directly modified by the method. Absent aliasing, no other expression has a different value after a call to the method. But checking of this annotation (under -AcheckPurityAnnotations) treats two expressions as possibly aliased only when an assignment relating them appears in the method body.

This annotation is inherited by subtypes, just as if it were meta-annotated with @InheritedAnnotation.

On a constructor, this annotation constrains what the constructor modifies besides the object being constructed. Assigning to the new object's own fields is always permitted and need not be listed, because the object did not exist before the call; writing this in the annotation is legal but has no additional effect. At a new expression, the expressions that are reached through this are ignored, because the object being constructed did not exist before the call. A constructor's annotation does not yet affect type refinement at new expressions.

See the Checker Framework Manual:
Checking

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    value
    An upper bound on the expressions that this method might change the value of.

  • Element Details

    • value

      @JavaExpression String[] value
      An upper bound on the expressions that this method might change the value of.

      Each expression must denote the same location every time it is evaluated: it must be a variable, a field access, an array access, a literal, a class name, or a call to a Pure method, recursively. A @Pure method returns the same value every time it is called with the same arguments, so a call to one qualifies so long as its receiver and its arguments do. An expression such as "#1.getList()", where getList is not @Pure, may denote a different value each time it is evaluated, so no method body could satisfy it.

      Returns:
      the Java expressions that the annotated method might side-effect
      See the Checker Framework Manual:
      Syntax of Java expressions