| import org.checkerframework.checker.nullness.qual.*; |
| import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; |
| |
| public class Asserts { |
| |
| void propogateToExpr() { |
| String s = "m"; |
| assert false : s.getClass(); |
| } |
| |
| void incorrectAssertExpr() { |
| String s = null; |
| assert s != null : "@AssumeAssertion(nullness)"; // error |
| s.getClass(); // OK |
| } |
| |
| void correctAssertExpr() { |
| String s = null; |
| assert s == null : "@AssumeAssertion(nullness)"; |
| // :: error: (dereference.of.nullable) |
| s.getClass(); // error |
| } |
| |
| class ArrayCell { |
| @Nullable Object[] vals = new @Nullable Object[0]; |
| } |
| |
| void assertComplexExpr(ArrayCell ac, int i) { |
| assert ac.vals[i] != null : "@AssumeAssertion(nullness)"; |
| @NonNull Object o = ac.vals[i]; |
| i = 10; |
| // :: error: (assignment) |
| @NonNull Object o2 = ac.vals[i]; |
| } |
| |
| boolean pairwiseEqual(boolean @Nullable [] seq1, boolean @Nullable [] seq2) { |
| if (!sameLength(seq1, seq2)) { |
| return false; |
| } |
| if (ne(seq1[0], seq2[0])) {} |
| return true; |
| } |
| |
| @EnsuresNonNullIf( |
| result = true, |
| expression = {"#1", "#2"}) |
| boolean sameLength(final boolean @Nullable [] seq1, final boolean @Nullable [] seq2) { |
| // don't bother with the implementation |
| // :: error: (contracts.conditional.postcondition) |
| return true; |
| } |
| |
| static boolean ne(boolean a, boolean b) { |
| return true; |
| } |
| |
| void testAssertBad(boolean @Nullable [] seq1, boolean @Nullable [] seq2) { |
| assert sameLength(seq1, seq2); |
| // the @EnsuresNonNullIf is not taken from the assert, as it doesn't contain "nullness" |
| // :: error: (accessing.nullable) |
| if (seq1[0]) {} |
| } |
| |
| void testAssertGood(boolean @Nullable [] seq1, boolean @Nullable [] seq2) { |
| assert sameLength(seq1, seq2) : "@AssumeAssertion(nullness)"; |
| // The explanation contains "nullness" and we therefore take the additional assumption |
| if (seq1[0]) {} |
| } |
| |
| void testAssertAnd(@Nullable Object o) { |
| assert o != null && o.hashCode() > 6; |
| } |
| |
| void testAssertOr(@Nullable Object o) { |
| // :: error: (dereference.of.nullable) |
| assert o != null || o.hashCode() > 6; |
| } |
| } |