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 static final long serialVersionUID = 20031024L; 013 014 /** 015 * Boolean. Set to true to disable all SeqIndex invariants (SeqIndexIntEqual, 016 * SeqIndexFloatLessThan, etc). This overrides the settings of the individual SeqIndex enable 017 * configuration options. To disable only some options, the options must be disabled individually. 018 */ 019 public static boolean dkconfig_SeqIndexDisableAll = false; 020 021 protected SingleSequence(PptSlice ppt) { 022 super(ppt); 023 } 024 025 protected @Prototype SingleSequence() { 026 super(); 027 } 028 029 public VarInfo var( 030 @GuardSatisfied @UnknownInitialization(SingleSequence.class) SingleSequence this) { 031 return ppt.var_infos[0]; 032 } 033}