java.lang.Object
org.checkerframework.checker.guieffect.Effect

public final class Effect extends Object
An effect -- either UIEffect, PolyUIEffect, or SafeEffect.
  • Constructor Details

    • Effect

      public Effect(Class<? extends Annotation> cls)
      Create a new Effect object.
      Parameters:
      cls - one of UIEffect.class, PolyUIEffect.class, or SafeEffect.class
  • Method Details

    • lessThanOrEqualTo

      public static boolean lessThanOrEqualTo(Effect left, Effect right)
      Return true iff left is less than or equal to right.
      Parameters:
      left - the first effect to compare
      right - the first effect to compare
      Returns:
      true iff left is less than or equal to right
    • min

      public static Effect min(Effect l, Effect r)
    • isSafe

      public boolean isSafe()
      Return true if this is SafeEffect.
      Returns:
      true if this is SafeEffect
    • isUI

      public boolean isUI()
      Return true if this is UIEffect.
      Returns:
      true if this is UIEffect
    • isPoly

      @Pure public boolean isPoly()
      Return true if this is PolyUIEffect.
      Returns:
      true if this is PolyUIEffect
    • getAnnot

      public Class<? extends Annotation> getAnnot()
    • toString

      @SideEffectFree public String toString()
      Overrides:
      toString in class Object
    • equals

      public boolean equals(Effect e)
      Return true if this equals the given effect.
      Parameters:
      e - the effect to compare this to
      Returns:
      true if this equals the given effect
    • equals

      public boolean equals(@Nullable Object o)
      Overrides:
      equals in class Object
    • hashCode

      @Pure public int hashCode()
      Overrides:
      hashCode in class Object