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  static final long serialVersionUID = 20030218L;
017
018  static @Nullable DummyInvariant dummyInvFactory;
019  private @Nullable DummyInvariant dummyInv;
020
021  private @Nullable VarInfo x_varinfo;
022
023  public SplitterExample() {}
024
025  public SplitterExample(Ppt ppt) {
026    x_varinfo = ppt.find_var_by_name("X");
027    instantiated = true;
028  }
029
030  @Override
031  public Splitter instantiateSplitter(Ppt ppt) {
032    return new SplitterExample(ppt);
033  }
034
035  @EnsuresNonNullIf(result = true, expression = "x_varinfo")
036  @Override
037  public boolean valid() {
038    return (x_varinfo != null);
039  }
040
041  @SuppressWarnings(
042      "nullness:contracts.precondition.override") // application invariant about private
043  // variable
044  @RequiresNonNull("x_varinfo")
045  @Override
046  public boolean test(ValueTuple vt) {
047    // Alternately, if x represents an array, use
048    //   vt.getIntArrayValue(x_varinfo);
049    return (x_varinfo.getIntValue(vt) > 0);
050  }
051
052  @Override
053  public String condition() {
054    return "X > 0";
055  }
056
057  @EnsuresNonNull("dummyInvFactory")
058  @Override
059  public void makeDummyInvariantFactory(DummyInvariant inv) {
060    assert dummyInvFactory == null;
061    dummyInvFactory = inv;
062  }
063
064  @RequiresNonNull("dummyInvFactory")
065  @Override
066  public void instantiateDummy(PptTopLevel ppt) {
067    dummyInv = null;
068    VarInfo x_vi = ppt.find_var_by_name("X");
069    if (x_vi != null) {
070      dummyInv = dummyInvFactory.instantiate(ppt, new VarInfo[] {x_vi});
071    }
072  }
073
074  @Override
075  public @Nullable DummyInvariant getDummyInvariant() {
076    return dummyInv;
077  }
078}