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}