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}