001package daikon.split;
002
003import daikon.Ppt;
004import daikon.PptTopLevel;
005import daikon.ValueTuple;
006import daikon.VarInfo;
007import daikon.inv.DummyInvariant;
008import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
009import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
010import org.checkerframework.checker.nullness.qual.Nullable;
011import org.checkerframework.checker.nullness.qual.RequiresNonNull;
012
013// This splitter tests the condition "X>0".
014@SuppressWarnings("nullness") // uses private fields, client code not analyzed
015public final class SplitterExample extends Splitter {
016  // We are Serializable, so we specify a version to allow changes to
017  // method signatures without breaking serialization.  If you add or
018  // remove fields, you should change this number to the current date.
019  static final long serialVersionUID = 20030218L;
020
021  static @Nullable DummyInvariant dummyInvFactory;
022  private @Nullable DummyInvariant dummyInv;
023
024  private @Nullable VarInfo x_varinfo;
025
026  public SplitterExample() {}
027
028  public SplitterExample(Ppt ppt) {
029    x_varinfo = ppt.find_var_by_name("X");
030    instantiated = true;
031  }
032
033  @Override
034  public Splitter instantiateSplitter(Ppt ppt) {
035    return new SplitterExample(ppt);
036  }
037
038  @EnsuresNonNullIf(result = true, expression = "x_varinfo")
039  @Override
040  public boolean valid() {
041    return (x_varinfo != null);
042  }
043
044  @SuppressWarnings(
045      "nullness:contracts.precondition.override") // application invariant about private
046  // variable
047  @RequiresNonNull("x_varinfo")
048  @Override
049  public boolean test(ValueTuple vt) {
050    // Alternately, if x represents an array, use
051    //   vt.getIntArrayValue(x_varinfo);
052    return (x_varinfo.getIntValue(vt) > 0);
053  }
054
055  @Override
056  public String condition() {
057    return "X > 0";
058  }
059
060  @EnsuresNonNull("dummyInvFactory")
061  @Override
062  public void makeDummyInvariantFactory(DummyInvariant inv) {
063    assert dummyInvFactory == null;
064    dummyInvFactory = inv;
065  }
066
067  @RequiresNonNull("dummyInvFactory")
068  @Override
069  public void instantiateDummy(PptTopLevel ppt) {
070    dummyInv = null;
071    VarInfo x_vi = ppt.find_var_by_name("X");
072    if (x_vi != null) {
073      dummyInv = dummyInvFactory.instantiate(ppt, new VarInfo[] {x_vi});
074    }
075  }
076
077  @Override
078  public @Nullable DummyInvariant getDummyInvariant() {
079    return dummyInv;
080  }
081}