| import org.checkerframework.checker.nullness.qual.*; |
| import org.checkerframework.checker.nullness.qual.EnsuresNonNull; |
| |
| public class AssertAfterChecked { |
| |
| class InitField { |
| @Nullable Object f; |
| |
| @EnsuresNonNull("f") |
| void init() { |
| f = new Object(); |
| } |
| |
| @EnsuresNonNull("f") |
| // :: error: (contracts.postcondition) |
| void initBad() {} |
| |
| void testInit() { |
| init(); |
| f.toString(); |
| } |
| } |
| |
| static class InitStaticField { |
| static @Nullable Object f; |
| |
| @EnsuresNonNull("f") |
| void init() { |
| f = new Object(); |
| } |
| |
| @EnsuresNonNull("f") |
| void init2() { |
| InitStaticField.f = new Object(); |
| } |
| |
| @EnsuresNonNull("f") |
| // :: error: (contracts.postcondition) |
| void initBad() {} |
| |
| void testInit() { |
| init(); |
| f.toString(); |
| } |
| |
| @EnsuresNonNull("InitStaticField.f") |
| void initE() { |
| f = new Object(); |
| } |
| |
| @EnsuresNonNull("InitStaticField.f") |
| void initE2() { |
| InitStaticField.f = new Object(); |
| } |
| |
| @EnsuresNonNull("InitStaticField.f") |
| // :: error: (contracts.postcondition) |
| void initBadE() {} |
| |
| void testInitE() { |
| initE(); |
| // TODO: we need to also support the unqualified static field access? |
| // f.toString(); |
| } |
| |
| void testInitE2() { |
| initE(); |
| InitStaticField.f.toString(); |
| } |
| } |
| |
| class TestParams { |
| @EnsuresNonNull("get(#1)") |
| // :: error: (contracts.postcondition) |
| void init(final TestParams p) {} |
| |
| @org.checkerframework.dataflow.qual.Pure |
| @Nullable Object get(Object o) { |
| return null; |
| } |
| |
| void testInit1() { |
| init(this); |
| get(this).toString(); |
| } |
| |
| void testInit1b() { |
| init(this); |
| this.get(this).toString(); |
| } |
| |
| void testInit2(TestParams p) { |
| init(p); |
| get(p).toString(); |
| } |
| |
| void testInit3(TestParams p) { |
| p.init(this); |
| p.get(this).toString(); |
| } |
| |
| void testInit4(TestParams p) { |
| p.init(this); |
| // :: error: (dereference.of.nullable) |
| this.get(this).toString(); |
| } |
| } |
| |
| class WithReturn { |
| @Nullable Object f; |
| |
| @EnsuresNonNull("f") |
| int init1() { |
| f = new Object(); |
| return 0; |
| } |
| |
| @EnsuresNonNull("f") |
| int init2() { |
| if (5 == 5) { |
| f = new Object(); |
| return 0; |
| } else { |
| f = new Object(); |
| return 1; |
| } |
| } |
| |
| @EnsuresNonNull("f") |
| // :: error: (contracts.postcondition) |
| int initBad1() { |
| return 0; |
| } |
| |
| @EnsuresNonNull("f") |
| // :: error: (contracts.postcondition) |
| int initBad2() { |
| if (5 == 5) { |
| return 0; |
| } else { |
| f = new Object(); |
| return 1; |
| } |
| } |
| |
| void testInit() { |
| init1(); |
| f.toString(); |
| } |
| } |
| } |