001package daikon.split.misc;
002
003import daikon.Ppt;
004import daikon.ProglangType;
005import daikon.ValueTuple;
006import daikon.VarInfo;
007import daikon.inv.DummyInvariant;
008import daikon.split.Splitter;
009import org.checkerframework.checker.initialization.qual.UnknownInitialization;
010import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
011import org.checkerframework.checker.nullness.qual.Nullable;
012import org.checkerframework.checker.nullness.qual.RequiresNonNull;
013
014// This splitter tests the condition "return == true".
015public final class ReturnTrueSplitter extends Splitter {
016  static final long serialVersionUID = 20020122L;
017
018  private @Nullable VarInfo return_varinfo;
019
020  /** Create a prototype (factory) splitter. */
021  public ReturnTrueSplitter() {}
022
023  /** Create a new instantiated ReturnTrueSplitter. */
024  public ReturnTrueSplitter(@UnknownInitialization(Ppt.class) Ppt ppt) {
025    return_varinfo = ppt.find_var_by_name("return");
026    instantiated = true;
027  }
028
029  @SuppressWarnings("nullness:return") // why is "new ...Splitter" @UnderInitialization?
030  @Override
031  public Splitter instantiateSplitter(@UnknownInitialization(Ppt.class) Ppt ppt) {
032    return new ReturnTrueSplitter(ppt);
033  }
034
035  @EnsuresNonNullIf(result = true, expression = "return_varinfo")
036  @Override
037  public boolean valid() {
038    return (return_varinfo != null) && (return_varinfo.type == ProglangType.BOOLEAN);
039  }
040
041  @SuppressWarnings(
042      "nullness:contracts.precondition.override") // application invariant about private
043  // variable
044  @RequiresNonNull("return_varinfo")
045  @Override
046  public boolean test(ValueTuple vt) {
047    return (return_varinfo.getIntValue(vt) != 0);
048  }
049
050  @Override
051  public String condition() {
052    return "return == true";
053  }
054
055  @Override
056  public @Nullable DummyInvariant getDummyInvariant() {
057    return null;
058  }
059}