| import org.checkerframework.checker.nullness.qual.*; |
| import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; |
| |
| public class AssertIfChecked { |
| |
| boolean unknown = false; |
| |
| @Nullable Object value; |
| |
| @EnsuresNonNullIf(result = true, expression = "value") |
| // :: error: (contracts.conditional.postcondition.returntype) |
| public void badform1() {} |
| |
| @EnsuresNonNullIf(result = true, expression = "value") |
| // :: error: (contracts.conditional.postcondition.returntype) |
| public Object badform2() { |
| return new Object(); |
| } |
| |
| @EnsuresNonNullIf(result = false, expression = "value") |
| // :: error: (contracts.conditional.postcondition.returntype) |
| public void badform3() {} |
| |
| @EnsuresNonNullIf(result = false, expression = "value") |
| // :: error: (contracts.conditional.postcondition.returntype) |
| public Object badform4() { |
| return new Object(); |
| } |
| |
| @EnsuresNonNullIf(result = true, expression = "value") |
| public boolean goodt1() { |
| return value != null; |
| } |
| |
| @EnsuresNonNullIf(result = true, expression = "value") |
| public boolean badt1() { |
| // :: error: (contracts.conditional.postcondition) |
| return value == null; |
| } |
| |
| @EnsuresNonNullIf(result = false, expression = "value") |
| public boolean goodf1() { |
| return value == null; |
| } |
| |
| @EnsuresNonNullIf(result = false, expression = "value") |
| public boolean badf1() { |
| // :: error: (contracts.conditional.postcondition) |
| return value != null; |
| } |
| |
| @EnsuresNonNullIf(result = true, expression = "value") |
| public boolean bad2() { |
| // :: error: (contracts.conditional.postcondition) |
| return value == null || unknown; |
| } |
| |
| @EnsuresNonNullIf(result = false, expression = "value") |
| public boolean bad3() { |
| // :: error: (contracts.conditional.postcondition) |
| return value == null && unknown; |
| } |
| |
| @EnsuresNonNullIf(result = true, expression = "#1") |
| boolean testParam(final @Nullable Object param) { |
| return param != null; |
| } |
| |
| @EnsuresNonNullIf(result = true, expression = "#1") |
| boolean testLitTTgood1(final @Nullable Object param) { |
| if (param == null) { |
| return false; |
| } |
| return true; |
| } |
| |
| @EnsuresNonNullIf(result = true, expression = "#1") |
| boolean testLitTTbad1(final @Nullable Object param) { |
| // :: error: (contracts.conditional.postcondition) |
| return true; |
| } |
| |
| @EnsuresNonNullIf(result = false, expression = "#1") |
| boolean testLitFFgood1(final @Nullable Object param) { |
| return true; |
| } |
| |
| @EnsuresNonNullIf(result = false, expression = "#1") |
| boolean testLitFFgood2(final @Nullable Object param) { |
| if (param == null) { |
| return true; |
| } |
| return false; |
| } |
| |
| @EnsuresNonNullIf(result = false, expression = "#1") |
| boolean testLitFFbad1(final @Nullable Object param) { |
| if (param == null) { |
| // :: error: (contracts.conditional.postcondition) |
| return false; |
| } |
| return true; |
| } |
| |
| @EnsuresNonNullIf(result = false, expression = "#1") |
| boolean testLitFFbad2(final @Nullable Object param) { |
| // :: error: (contracts.conditional.postcondition) |
| return false; |
| } |
| |
| @Nullable Object getValueUnpure() { |
| return value; |
| } |
| |
| @org.checkerframework.dataflow.qual.Pure |
| @Nullable Object getValuePure() { |
| return value; |
| } |
| |
| @EnsuresNonNullIf(result = true, expression = "getValuePure()") |
| public boolean hasValuePure() { |
| return getValuePure() != null; |
| } |
| |
| @EnsuresNonNullIf(result = true, expression = "#1") |
| public static final boolean isComment(@Nullable String s) { |
| return s != null && (s.startsWith("//") || s.startsWith("#")); |
| } |
| |
| @EnsuresNonNullIf(result = true, expression = "#1") |
| public boolean myEquals(@Nullable Object o) { |
| return (o instanceof String) && equals((String) o); |
| } |
| |
| /* |
| * The next two methods are from Daikon's class Quant. They verify that |
| * EnsuresNonNullIf is correctly added to the assumptions after a check. |
| */ |
| |
| @EnsuresNonNullIf( |
| result = true, |
| expression = {"#1", "#2"}) |
| /* pure */ public static boolean sameLength( |
| boolean @Nullable [] seq1, boolean @Nullable [] seq2) { |
| return ((seq1 != null) && (seq2 != null) && seq1.length == seq2.length); |
| } |
| |
| /* pure */ public static boolean isReverse(boolean @Nullable [] seq1, boolean @Nullable [] seq2) { |
| if (!sameLength(seq1, seq2)) { |
| return false; |
| } |
| // This assert is not needed for inference. |
| // assert seq1 != null && seq2 != null; // because sameLength() = true |
| |
| int length = seq1.length; |
| for (int i = 0; i < length; i++) { |
| if (seq1[i] != seq2[length - i - 1]) { |
| return false; |
| } |
| } |
| return true; |
| } |
| } |