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}