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
|
Description: Add the checkerframework annotations (not yet packaged in Debian)
Author: Emmanuel Bourg <ebourg@apache.org>
Forwarded: not-needed
--- /dev/null
+++ b/guava/src/org/checkerframework/checker/nullness/qual/Nullable.java
@@ -0,0 +1,26 @@
+package org.checkerframework.checker.nullness.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * {@link Nullable} is a type annotation that indicates that the value is not
+ * known to be non-null (see {@link NonNull}). Only if an expression has a
+ * {@link Nullable} type may it be assigned {@code null}.
+ *
+ * <p>
+ * This annotation is associated with the {@link AbstractNullnessChecker}.
+ *
+ * @see NonNull
+ * @see MonotonicNonNull
+ * @see AbstractNullnessChecker
+ * @checker_framework.manual #nullness-checker Nullness Checker
+ */
+@Documented
+@Retention(RetentionPolicy.SOURCE)
+@Target({ ElementType.TYPE_USE, ElementType.TYPE_PARAMETER })
+public @interface Nullable {
+}
--- /dev/null
+++ b/guava/src/org/checkerframework/checker/nullness/qual/MonotonicNonNull.java
@@ -0,0 +1,56 @@
+package org.checkerframework.checker.nullness.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that a field (or variable) is lazily initialized to a non-null
+ * value. Once the field becomes non-null, it never becomes null again.
+ * There is no guarantee that the field ever becomes non-null, but if it
+ * does, it will stay non-null.
+ * <p>
+ *
+ * A monotonically non-null field has these two properties:
+ * <ol>
+ * <li>The field may be assigned only non-null values.</li>
+ * <li>The field may be re-assigned as often as desired.</li>
+ * </ol>
+ * <p>
+ *
+ * When the field is first read within a method, the field cannot be
+ * assumed to be non-null. After a check that a {@code MonotonicNonNull} field
+ * holds a non-null value, all subsequent accesses <em>within that
+ * method</em> can be assumed to be non-null, even after arbitrary external
+ * method calls that might access the field.
+ * <p>
+ *
+ * {@code MonotonicNonNull} gives stronger guarantees than {@link Nullable}.
+ * After a check that a {@link Nullable} field holds a non-null value, only
+ * accesses until the next non-{@link org.checkerframework.dataflow.qual.SideEffectFree} method is called can be assumed
+ * to be non-null.
+ * <p>
+ *
+ * To indicate that a {@code MonotonicNonNull} or {@code Nullable} field is
+ * non-null whenever a particular method is called, use
+ * {@link RequiresNonNull}.
+ * <p>
+ *
+ * Final fields are treated as MonotonicNonNull by default.
+ * <p>
+ *
+ * This annotation is associated with the {@link AbstractNullnessChecker}.
+ *
+ * @see EnsuresNonNull
+ * @see RequiresNonNull
+ * @see MonotonicQualifier
+ * @see AbstractNullnessChecker
+ * @checker_framework.manual #nullness-checker Nullness Checker
+ */
+@Documented
+@Target(ElementType.TYPE_USE)
+@Retention(RetentionPolicy.SOURCE)
+public @interface MonotonicNonNull {
+}
--- /dev/null
+++ b/guava/src/org/checkerframework/checker/nullness/qual/NonNull.java
@@ -0,0 +1,41 @@
+package org.checkerframework.checker.nullness.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+import javax.lang.model.type.TypeKind;
+
+/**
+ * {@link NonNull} is a type annotation that indicates that an expression is
+ * never {@code null}.
+ *
+ * <p>
+ * For fields of a class, the {@link NonNull} annotation indicates that this
+ * field is never {@code null}
+ * <em>after the class has been fully initialized</em>. Class initialization is
+ * controlled by the Freedom Before Commitment type system, see
+ * {@link InitializationChecker} for more details.
+ *
+ * <p>
+ * For static fields, the {@link NonNull} annotation indicates that this field
+ * is never {@code null} <em>after the containing class is initialized</em>.
+ *
+ * <p>
+ * This annotation is rarely written in source code, because it is the default.
+ *
+ * <p>
+ * This annotation is associated with the {@link AbstractNullnessChecker}.
+ *
+ * @see Nullable
+ * @see MonotonicNonNull
+ * @see AbstractNullnessChecker
+ * @checker_framework.manual #nullness-checker Nullness Checker
+ */
+@Documented
+@Retention(RetentionPolicy.SOURCE)
+@Target({ ElementType.TYPE_USE, ElementType.TYPE_PARAMETER })
+public @interface NonNull {
+}
|
