001package daikon.inv.unary.sequence;
002
003import daikon.PptSlice;
004import daikon.VarInfo;
005import daikon.inv.unary.UnaryInvariant;
006import org.checkerframework.checker.initialization.qual.UnknownInitialization;
007import org.checkerframework.checker.lock.qual.GuardSatisfied;
008import typequals.prototype.qual.Prototype;
009
010/** Invariants on a single sequence (array) variable, such as {@code a[] contains no duplicates}. */
011public abstract class SingleSequence extends UnaryInvariant {
012  // We are Serializable, so we specify a version to allow changes to
013  // method signatures without breaking serialization.  If you add or
014  // remove fields, you should change this number to the current date.
015  static final long serialVersionUID = 20031024L;
016
017  /**
018   * Boolean. Set to true to disable all SeqIndex invariants (SeqIndexIntEqual,
019   * SeqIndexFloatLessThan, etc). This overrides the settings of the individual SeqIndex enable
020   * configuration options. To disable only some options, the options must be disabled individually.
021   */
022  public static boolean dkconfig_SeqIndexDisableAll = false;
023
024  protected SingleSequence(PptSlice ppt) {
025    super(ppt);
026  }
027
028  protected @Prototype SingleSequence() {
029    super();
030  }
031
032  public VarInfo var(
033      @GuardSatisfied @UnknownInitialization(SingleSequence.class) SingleSequence this) {
034    return ppt.var_infos[0];
035  }
036}