File: AssertAfterChecked.java

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 23,104 kB
  • sloc: java: 145,916; xml: 839; sh: 518; makefile: 404; perl: 26
file content (151 lines) | stat: -rw-r--r-- 3,415 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
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.not.satisfied)
        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.not.satisfied)
        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.not.satisfied)
        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.not.satisfied)
        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.not.satisfied)
        int initBad1() {
            return 0;
        }

        @EnsuresNonNull("f")
        // :: error: (contracts.postcondition.not.satisfied)
        int initBad2() {
            if (5 == 5) {
                return 0;
            } else {
                f = new Object();
                return 1;
            }
        }

        void testInit() {
            init1();
            f.toString();
        }
    }
}