File: warnings.tex

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 (800 lines) | stat: -rw-r--r-- 35,427 bytes parent folder | download | duplicates (2)
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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
\htmlhr
\chapterAndLabel{Suppressing warnings}{suppressing-warnings}

%% This feels redundant.
% The Checker Framework is sound:  whenever your code contains an error, the
% Checker Framework will warn you about the error.  The Checker Framework is
% conservative:  it may issue warnings when your code is safe and never
% misbehaves at run time.

When the Checker Framework reports a warning, it's best to fix the
underlying problem, by changing the code or its annotations.  For each
warning, follow the methodology in Section~\ref{handling-warnings} to
correct the underlying problem.

This section describes what to do if the methodology of
Section~\ref{handling-warnings} indicates that you need to suppress the
warning.  You won't change your code, but you will prevent the Checker
Framework from reporting this particular warning to you.  (Changing the
code to fix a bug is another way to prevent the Checker Framework from
issuing a warning, but it is not what this chapter is about.)

You may wish to suppress checker warnings because of unannotated libraries
or un-annotated portions of your own code, because of application
invariants that are beyond the capabilities of the type system, because of
checker limitations, because you are interested in only some of the
guarantees provided by a checker, or for other reasons.
Suppressing a warning is similar to writing a cast in a Java
program:  the programmer knows more about the type than the type system does
and uses the warning suppression or cast to convey that information to the
type system.

You can suppress a warning message in a single variable initializer,
method, or class by using the following mechanisms:

\newcounter{lastsinglesuppression}
\begin{itemize}
\item
  the \code{@SuppressWarnings} annotation
  (Section~\ref{suppresswarnings-annotation}), or
\item
  the \code{@AssumeAssertion} string in an \<assert> message (Section~\ref{assumeassertion}).
\end{itemize}

You can suppress warnings throughout the codebase by using the following mechanisms:

\begin{itemize}
\item
  the \code{-AsuppressWarnings} command-line option (Section~\ref{suppresswarnings-command-line}),
\item
  the \code{-AskipUses} and \code{-AonlyUses} command-line options (Section~\ref{askipuses}),
\item
  the \code{-AskipDefs} and \code{-AonlyDefs} command-line options (Section~\ref{askipdefs}),
\item
  the \code{-AuseDefaultsForUncheckedCode=source} command-line
  option (Section~\ref{compiling-libraries}),
\item
  the \code{-Alint} command-line option enables/disables optional checks (Section~\ref{alint}), or
\item
  not running the annotation processor
  (Section~\ref{no-processor}).
\end{itemize}

Some type checkers can suppress warnings via
\begin{itemize}
\item
  checker-specific mechanisms (Section~\ref{checker-specific-suppression}).
\end{itemize}

\noindent
The rest of this chapter explains these mechanisms in turn.

You can use the \code{-AwarnUnneededSuppressions} command-line option to issue a
warning if a \code{@SuppressWarnings} did not suppress any warnings issued by the current checker.

% See the @SuppressWarningsKey annotation and the getSuppressWarningsKey method.

\sectionAndLabel{\code{@SuppressWarnings} annotation}{suppresswarnings-annotation}

\begin{sloppypar}
You can suppress specific errors and warnings by use of the
\code{@SuppressWarnings} annotation, for example
\code{@SuppressWarnings("interning")} or \code{@SuppressWarnings("nullness")}.
Section~\ref{suppresswarnings-annotation-syntax} explains the syntax of the
argument string.
\end{sloppypar}

A \sunjavadocanno{java.base/java/lang/SuppressWarnings.html}{SuppressWarnings}
annotation may be placed on program declarations such as a local
variable declaration, a method, or a class.  It suppresses all warnings
within that program element.
Section~\ref{suppresswarnings-annotation-locations} discusses where the
annotation may be written in source code.

Section~\ref{suppresswarnings-best-practices} gives best practices for
writing \<@SuppressWarnings> annotations.


\subsectionAndLabel{\code{@SuppressWarnings} syntax}{suppresswarnings-annotation-syntax}

The \code{@SuppressWarnings} annotation takes a string argument, in one of
the following forms:
\code{"\emph{checkername}:\emph{messagekey}"},
\code{"\emph{checkername}"},
or
\code{"\emph{messagekey}"}.

The argument \emph{checkername} is
in lower case and is derived from the way you invoke the checker.  For
example, if you invoke a checker as
\code{javac -processor MyNiftyChecker ...},
then you would suppress its error messages with
\code{@SuppressWarnings("mynifty")}.  (An exception is the Subtyping
Checker, for which you use the annotation name; see
Section~\ref{subtyping-using}.)
Sometimes, a checker honors \emph{checkername} arguments; use
the \code{-AshowSuppressWarningKeys} command-line option to see them.
Using \code{"all"} as the checkername applies to all checkers; this is not
recommended, except for messages common to all checkers such as
purity-related messages when using \<-AcheckPurityAnnotations>.

The argument \emph{messagekey} is the message key for the error.
Each warning message from the compiler gives the most specific
suppression key that can be used to suppress that warning.
An example is \<dereference.of.nullable> in

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
MyFile.java:107: error: [dereference.of.nullable] dereference of possibly-null reference myList
          myList.add(elt);
          ^
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX

\noindent
You are allowed to use any substring of a message key.  Beware writing a very
short messagekey, because it might suppress more warnings than you expect.

If the \emph{checkername} part is omitted, the \<@SuppressWarnings> applies
to all checkers.
If the \emph{messagekey} part is omitted, the \<@SuppressWarnings> applies
to all messages (it suppresses all warnings from the given checker).

With the \code{-ArequirePrefixInWarningSuppressions} command-line
option, a warning is only suppressed if the key is in the
\code{"\emph{checkername}"} or
\code{"\emph{checkername}:\emph{messagekey}"}
format, as in
\<@SuppressWarnings("nullness")> or
\<@SuppressWarnings("nullness:assignment.type.incompatible")>.

%% This is true, but relevant mostly to developers, not users.
% For a list of all message keys for a given checker, see two files:
% \begin{enumerate}
% \item \code{checker-framework/checker/src/org/checkerframework/checker/\emph{checkername}/messages.properties}
% \item \code{checker-framework/framework/src/org/checkerframework/common/basetype/messages.properties}
% \end{enumerate}
%
% \noindent
% You need to check the latter file because
% each checker is built on the \code{basetype} checker and inherits its
% properties.


\subsectionAndLabel{Where \code{@SuppressWarnings} can be written}{suppresswarnings-annotation-locations}

\<@SuppressWarnings> is a declaration annotation, so it may be placed on
program declarations such as a local variable declaration, a method, or a
class.  It cannot be used on statements, expressions, or types.
(\<assert> plus \<@AssumeAssertion> can be used between statements and can
affect arbitrary expressions; see Section~\ref{assumeassertion}.)

Always write a \<@SuppressWarnings> annotation on the smallest possible
scope.  To reduce the scope of a \<@SuppressWarnings> annotation, it is
sometimes desirable to refactor the code.  You might extract an expression
into a local variable, so that warnings can be suppressed just for that
local variable's initializer expression.  Likewise, you might extract some
code into a separate method, so that warnings can be suppressed just for
its body.  Or, you can use \<@AssumeAssertion> on an \<assert> statement;
see Section~\ref{assumeassertion}.

As an example, consider suppressing a warning at an assignment that you know is
safe.  Here is an example that uses the Tainting Checker
(Section~\ref{tainting-checker}).  Assume that \<expr> has compile-time
(declared) type \<@Tainted String>, but you know that the run-time value of
\<expr> is untainted.

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
  @SuppressWarnings("tainting:cast.unsafe") // expr is untainted because ... [explanation goes here]
  @Untainted String myvar = expr;
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX

\noindent
Java does not permit annotations (such as \<@SuppressWarnings>) on
assignments (or on other statements or expressions), so
it would have been \emph{illegal} to write

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
  @Untainted String myvar;
  ...
  @SuppressWarnings("tainting:cast.unsafe") // expr is untainted because ...
  myvar = expr;
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX


\subsectionAndLabel{Good practices when suppressing warnings}{suppresswarnings-best-practices}

\subsubsectionAndLabel{Suppress warnings in the smallest possible scope}{suppresswarnings-best-practices-smallest-scope}

Prefer \<@SuppressWarnings> on a local variable to one on a method, and
prefer one on a method to one on a class.

You may be able to suppress a warning about a use of an expression by
writing \<@AssumeAssertion> for the expression, before the use.  See
Section~\ref{assumeassertion}.

Another way to reduce the scope of a \<@SuppressWarnings> is to
extract the expression into a new local variable
and place a \code{@SuppressWarnings} annotation on the variable
declaration.  See Section~\ref{suppresswarnings-annotation-locations}.

%% I'm not sure how this is related to the smallest possible scope.
% As another example, if you have annotated the signatures but not the bodies
% of the methods in a class or package, put a \code{@SuppressWarnings}
% annotation on the class declaration or on the package's
% \code{package-info.java} file.


\subsubsectionAndLabel{Use a specific argument to \code{@SuppressWarnings}}{suppresswarnings-best-practices-specific-argument}


\label{compiler-message-keys}

It is best to use the most specific possible message key to suppress just a
specific error that you know to be a false positive.  The checker outputs
this message key when it issues an error.  If you use a broader
\<@SuppressWarnings> annotation, then it may mask other errors that you
needed to know about.

Any of the following would have suppressed the warning in
Section~\ref{suppresswarnings-annotation-locations}:

\begin{Verbatim}
  @SuppressWarnings("tainting")              // suppresses all tainting-related warnings
  @SuppressWarnings("cast")                  // suppresses warnings from all checkers about casts
  @SuppressWarnings("unsafe")                // suppresses warnings from all checkers about unsafe code
  @SuppressWarnings("cast.unsafe")           // suppresses warnings from all checkers about unsafe casts
  @SuppressWarnings("tainting:cast")         // suppresses tainting warnings about casts
  @SuppressWarnings("tainting:unsafe")       // suppresses tainting warnings about unsafe code
  @SuppressWarnings("tainting:cast.unsafe")  // suppresses tainting warnings about unsafe casts
\end{Verbatim}

The last one is the most specific, and therefore is the best style.


\subsubsectionAndLabel{Justify why the warning is a false positive}{suppresswarnings-best-practices-justification}

A \<@SuppressWarnings> annotation asserts that the programmer knows that
the code is actually correct or safe (that is, no undesired behavior will
occur), even though the type system is unable to prove that the code is
correct or safe.

Whenever you write a \<@SuppressWarnings> annotation, you should also
write, typically on the same line, a code comment
explaining why the code is actually correct.  In some cases you might also
justify why the code cannot be rewritten in a simpler way that would be
amenable to type-checking.  Also make it clear what error is being
suppressed.  (This is particularly important when the \<@SuppressWarnings> is
on a method declaration and the suppressed warning might be anywhere in the
method body.)

This documentation will help you and others to understand the reason for
the \<@SuppressWarnings> annotation.  It will also help you audit your code
to verify all the warning suppressions.  (The code is correct only if the
checker issues no warnings \emph{and} each \<@SuppressWarnings> is correct.)

A suppression message like ``a.f is not null'' is not useful.  The fact
that you are suppressing the warning means that you believe that \<a.f> is
not null.  The message should explain \emph{why} you believe that; for
example, ``a.f was checked above and no subsequent side effect can affect it''.

Here are some terse examples from libraries in \href{https://github.com/plume-lib/}{plume-lib}:

\begin{Verbatim}
@SuppressWarnings("cast") // cast is redundant (except when checking nullness)
@SuppressWarnings("interning") // FbType.FREE is interned but is not annotated
@SuppressWarnings("interning") // equality testing optimization
@SuppressWarnings("nullness") // used portion of array is non-null
@SuppressWarnings("nullness") // oi.factory is a static method, so null first argument is OK
@SuppressWarnings("purity") // side effect to local state of type BitSet
\end{Verbatim}

A particularly good (and concise) justification is to reference an issue in
the issue tracker, as in these two from \href{https://plse.cs.washington.edu/daikon/}{Daikon}:

\begin{Verbatim}
@SuppressWarnings("flowexpr.parse.error") // https://tinyurl.com/cfissue/862
@SuppressWarnings("keyfor") // https://tinyurl.com/cfissue/877
\end{Verbatim}

\noindent
Please report false positive warnings, then reference them in your warning suppressions.
This permits the Checker Framework maintainers to know about the
problem, it helps them with prioritization (by knowing how often in your
codebase a particular issue arises), and it enables you to know when an
issue has been fixed (though the \<-AwarnUnneededSuppressions> command-line
option also serves the latter purpose).


\sectionAndLabel{\code{@AssumeAssertion} string in an \<assert> message}{assumeassertion}

\begin{sloppypar}
You can suppress a warning by \<assert>ing that some property is true, and
placing the string \<@AssumeAssertion(\emph{warningkey})> in the assertion
message.
\end{sloppypar}

For example, in this code:

\begin{Verbatim}
while (c != Object.class) {
  ...
  c = c.getSuperclass();
  assert c != null
    : "@AssumeAssertion(nullness): c was not Object, so its superclass is not null";
 }
\end{Verbatim}

\noindent
the Nullness Checker assumes that \<c> is non-null from the \<assert>
statement forward (including on the next iteration through the loop).

The \<assert> expression must be an expression that would affect flow-sensitive
type refinement (Section~\ref{type-refinement}), if the
expression appeared in a conditional test.  Each type system has its own
rules about what type refinement it performs.

The warning key is exactly as in the \<@SuppressWarnings> annotation
(Section~\ref{suppresswarnings-annotation}).  The same good practices apply
as for \<@SuppressWarnings> annotations, such as writing a comment
justifying why the assumption is safe
(Section~\ref{suppresswarnings-best-practices}).
Sometimes, writing an assertion and \<@AssumeAssertion> is a less
disruptive code change than refactoring to create a location where
\<@SuppressWarnings> can be written.

The \<-AassumeAssertionsAreEnabled> and \<-AassumeAssertionsAreDisabled>
command-line options (Section~\ref{type-refinement-assertions}) do not
affect processing of \<assert> statements that have \<@AssumeAssertion> in
their message.  Writing \<@AssumeAssertion> means that the assertion would
succeed if it were executed, and the Checker Framework makes use of that
information regardless of the \<-AassumeAssertionsAreEnabled> and
\<-AassumeAssertionsAreDisabled> command-line options.


%% Redundant.
% If the string \<@AssumeAssertion(\emph{warningkey})> does not appear in the
% assertion message, then the Checker Framework treats the assertion as
% being used for defensive programming.  That is, the programmer believes
% that the assertion might fail at run time, so the Checker Framework should
% not make any inference, which would not be justified.

%% Users should never see assertions anyway -- they are for programmers.
% A downside of putting the string in the assertion message is that if the
% assertion ever fails, then a user might see the string and be confused.
% This should never be a problem, since
% the programmer should write the string should only if the programmer has
% reasoned that the
% assertion can never fail.

% (Another way of stating the Nullness Checker's use of assertions is as an
% additional caveat to the guarantees provided by a checker
% (Section~\ref{checker-guarantees}).  The Nullness Checker prevents null
% pointer errors in your code under the assumption that assertions are
% enabled, and it does not guarantee that all of your assertions succeed.)


\subsectionAndLabel{Suppressing warnings and defensive programming}{defensive-programming}

This section explains the distinction between two different uses for
assertions (and for related methods like JUnit's \<Assert.assertNotNull>).

Assertions are commonly used for two distinct purposes:  documenting how
the program works and debugging the program when it does not work
correctly.  By default, the Checker Framework assumes that each assertion
is used for debugging:  the assertion might fail at run time, and the programmer
wishes to be informed at compile time about such possible run-time errors.  On
the other hand, if you write the \<@AssumeAssertion> string in the \<assert>
message, then the Checker Framework assumes that you have used some other
technique to verify that the assertion can never fail at run time, so the
checker assumes the assertion passes and does not issue a warning.

Distinguishing the purpose of each assertion is important for precise
type-checking.
% In particular, the Checker Framework would miss many errors
% if it assumed that every assertion succeeds at run time.
Suppose that a
programmer encounters a failing test, adds an assertion to aid debugging, and fixes the
test.  The programmer leaves the assertion in the program if the programmer
is worried that the program might fail in a similar way in the future.
% The assertion indicates the potential for failure at this point in the code.
The Checker Framework should not assume that the assertion succeeds ---
doing so would defeat the very purpose of the Checker Framework, which is
to detect errors at compile time and prevent them from occurring at run
time.

On the other hand, assertions sometimes document facts that a programmer
has independently verified to be true, and the Checker Framework can
leverage these assertions in order to avoid issuing false positive
warnings.  The programmer marks such assertions with the \<@AssumeAssertion>
string in the \<assert> message.  Only do so if you are sure
that the assertion always succeeds at run time.


% In each case, the assertion or method indicates an application invariant --- a
% fact that should always be true.  There are two distinct reasons a
% programmer may have written the invariant, depending on whether the
% programmer is 100\% sure that the application invariant holds.
%
% \begin{enumerate}
% \item
%   A programmer might write it as \textbf{defensive programming}.  This causes
%   the program to throw an exception, which is useful for debugging because
%   it gives an earlier run-time indication of the error.
%   A programmer would use an assertion in this way if the programmer is not
%   100\% sure that the application invariant holds.
%
%   % , or even to document what the program
%   % is intended to do.
%
% \item
%   A programmer might write it to \textbf{suppress} false positive
%   \textbf{warning messages} from a checker.  A programmer would use an
%   assertion this way if the programmer is 100\% sure that the application
%   invariant holds, and the reference can never be null at run time.
%
% \end{enumerate}


Sometimes methods such as
\refmethod{checker/nullness}{NullnessUtil}{castNonNull}{-T-} are used
instead of assertions.  Just as for assertions, you can treat them as
debugging aids or as documentation.
If you know that a particular codebase uses
a nullness-checking method not for defensive programming but to indicate
facts that are guaranteed to be true (that is, these assertions will never
fail at run time), then you can suppress
warnings related to it.
Annotate its definition just as
\refmethod{checker/nullness}{NullnessUtil}{castNonNull}{-T-} is annotated (see the
source code for the Checker Framework).
% TODO:
% For an assert statement, XXXXX.
Also, be sure to document the intention in the method's Javadoc, so that
programmers do not
accidentally misuse it for defensive programming.


If you are annotating a codebase that already contains precondition checks,
such as:

\begin{Verbatim}
  public String get(String key, String def) {
    checkNotNull(key, "key"); // NOI18N
    ...
  }
\end{Verbatim}

\noindent
then you should mark the appropriate parameter as \<@NonNull> (which is the
default).  This will prevent the checker from issuing a warning about the
\<checkNotNull> call.



\sectionAndLabel{\code{-AsuppressWarnings} command-line option}{suppresswarnings-command-line}

Supplying the \<-AsuppressWarnings> command-line option is equivalent to
writing a \<@SuppressWarnings> annotation on every class that the compiler
type-checks.  The argument to \<-AsuppressWarnings> is a comma-separated
list of warning suppression keys, as in
\<-AsuppressWarnings=purity,uninitialized>.

When possible, it is better to write a \<@SuppressWarnings> annotation with a
smaller scope, rather than using the \<-AsuppressWarnings> command-line option.


\sectionAndLabel{\code{-AskipUses} and \code{-AonlyUses} command-line options}{askipuses}

You can suppress all errors and warnings at all \emph{uses} of a given
class, or suppress all errors and warnings except those at uses of a given
class.  (The class itself is still type-checked, unless you also use
the \code{-AskipDefs} or \code{-AonlyDefs} command-line option, see~\ref{askipdefs}).

Set the \code{-AskipUses} command-line option to a
regular expression that matches class names (not file names) for which warnings and errors
should be suppressed.
Or, set the \code{-AonlyUses} command-line option to a
regular expression that matches class names (not file names) for which warnings and errors
should be emitted; warnings about uses of all other classes will be suppressed.

For example, suppose that you use
``{\codesize\verb|-AskipUses=^java\.|}'' on the command line
(with appropriate quoting) when invoking
\code{javac}.  Then the checkers will suppress all warnings related to
classes whose fully-qualified name starts with \codesize\verb|java.|, such
as all warnings relating to invalid arguments and all warnings relating to
incorrect use of the return value.

To suppress all errors and warnings related to multiple classes, you can use
the regular expression alternative operator ``\code{|}'', as in
``{\codesize\verb+-AskipUses="java\.lang\.|java\.util\."+}'' to suppress
all warnings related to uses of classes that belong to the \code{java.lang} or
\code{java.util} packages.  (Depending on your shell or other tool, you
might need to change or remove the quoting.)

You can supply both \code{-AskipUses} and \code{-AonlyUses}, in which case
the \code{-AskipUses} argument takes precedence, and \code{-AonlyUses} does
further filtering but does not add anything that \code{-AskipUses} removed.

Warning:  Use the \code{-AonlyUses} command-line option with care,
because it can have unexpected results.  For example, if the
given regular expression does not match classes in the JDK, then the
Checker Framework will suppress every warning that involves a JDK class
such as \<Object> or \<String>.  The meaning of \code{-AonlyUses} may be
refined in the future.  Oftentimes \code{-AskipUses} is more useful.

% The desired meaning of -AonlyUses is tricky, because what is a "use"?
% Maybe only check calls of methods on the class (though don't check
% argument expressions) and field accesses, but nothing else (such as
% extends clauses that happen to use the class).  But then we would also
% want to suppress warnings related to assignments where a method use or
% field access is the right-hand side.  I'm going to punt on this for now.


\sectionAndLabel{\code{-AskipDefs} and \code{-AonlyDefs} command-line options}{askipdefs}

You can suppress all errors and warnings in the \emph{definition} of a given
class, or suppress all errors and warnings except those in the definition
of a given class.  (Uses of the class are still type-checked, unless you also use
the \code{-AskipUses} or \code{-AonlyUses} command-line option,
see~\ref{askipuses}.)

Set the \code{-AskipDefs} command-line option to a
regular expression that matches class names (not file names) in whose definition warnings and errors
should be suppressed.
Or, set the \code{-AonlyDefs} command-line option to a
regular expression that matches class names (not file names) whose
definitions should be type-checked.

For example, if you use
``{\codesize\verb|-AskipDefs=^mypackage\.|}'' on the command line
(with appropriate quoting) when invoking
\code{javac}, then the definitions of
classes whose fully-qualified name starts with \codesize\verb|mypackage.|
will not be checked.

If you supply both \code{-AskipDefs} and \code{-AonlyDefs}, then
\code{-AskipDefs} takes precedence.

Another way not to type-check a file is not to pass it on the compiler
command-line:  the Checker Framework type-checks only files that are passed
to the compiler on the command line, and does not type-check any file that
is not passed to the compiler.  The \code{-AskipDefs} and \code{-AonlyDefs}
command-line options
are intended for situations in which the build system is hard to understand
or change.  In such a situation, a programmer may find it easier to supply
an extra command-line argument, than to change the set of files that is
compiled.

A common scenario for using the arguments is when you are starting out by
type-checking only part of a legacy codebase.  After you have verified the
most important parts, you can incrementally check more classes until you
are type-checking the whole thing.


\sectionAndLabel{\code{-Alint} command-line option\label{lint-options}}{alint}

The \code{-Alint} option enables or disables optional checks, analogously to
javac's \code{-Xlint} option.
Each of the distributed checkers supports at least the following lint
options (and possibly more, see the checker's documentation):

% For the current list of lint options supported by all checkers, see
% method BaseTypeChecker.getSupportedLintOptions().

% For the per-checker list, search for "@SupportedLintOptions" in the
% checker implementations.


\begin{itemize}

\item
  \code{cast:unsafe} (default: on) warn about unsafe casts that are not
  checked at run time, as in \code{((@NonNull String) myref)}.  Such casts
  are generally not necessary because of type refinement
  (Section~\ref{type-refinement}).

\item
  \code{cast:redundant} (default: on) warn about redundant
  casts that are guaranteed to succeed at run time,
  as in \code{((@NonNull String) "m")}.  Such casts are not necessary,
  because the target expression of the cast already has the given type
  qualifier.

\item
  \code{cast} Enable or disable all cast-related warnings.

\item
\begin{sloppypar}
  \code{all} Enable or disable all lint warnings, including
  checker-specific ones if any.  Examples include \code{redundantNullComparison} for the
  Nullness Checker (see Section~\ref{nullness-lint-nulltest}) and \<dotequals> for
  the Interning Checker (see Section~\ref{lint-dotequals}).  This option
  does not enable/disable the checker's standard checks, just its optional
  ones.
\end{sloppypar}

\item
  \code{none} The inverse of \<all>:  disable or enable all lint warnings,
  including checker-specific ones if any.

\end{itemize}

% This syntax is different from -Xlint that uses a colon instead of an
% equals sign, because javac forces the use of the equals sign.

\noindent
To activate a lint option, write \code{-Alint=} followed by a
comma-delimited list of check names.  If the option is preceded by a
hyphen (\code{-}), the warning is disabled.  For example, to disable all
lint options except redundant casts, you can pass
\code{-Alint=-all,cast:redundant} on the command line.

Only the last \code{-Alint} option is used; all previous \code{-Alint}
options are silently ignored.  In particular, this means that \<-Alint=all
-Alint=cast:redundant> is \emph{not} equivalent to
\code{-Alint=-all,cast:redundant}.


\sectionAndLabel{Don't run the processor}{no-processor}

You can compile parts of your code without use of the
\code{-processor} switch to \code{javac}.  No checking is done during
such compilations, so no warnings are issued related to pluggable
type-checking.

You can direct your build system to avoid compiling certain parts of your
code.  For example, the \<-Dmaven.test.skip=true> command-line argument
tells Maven not to compile (or run) the tests.


\sectionAndLabel{Checker-specific mechanisms}{checker-specific-suppression}

Finally, some checkers have special rules.  For example, the Nullness
checker (Chapter~\ref{nullness-checker}) uses
the special \<castNonNull> method to suppress warnings
(Section~\ref{suppressing-warnings-with-assertions}).
This manual also explains special mechanisms for
suppressing warnings issued by the Fenum Checker
(Section~\ref{fenum-suppressing}) and the Units Checker
(Section~\ref{units-suppressing}).



\htmlhr
\chapterAndLabel{Handling legacy code}{legacy-code}

Section~\ref{get-started-with-legacy-code} describes a methodology for
applying annotations to legacy code.  This chapter tells you what to do if,
for some reason, you cannot change your code in such a way as to eliminate
a checker warning.

Also recall that you can convert checker errors into warnings via the
\code{-Awarns} command-line option; see Section~\ref{checker-options}.


\sectionAndLabel{Checking partially-annotated programs:  handling unannotated code}{unannotated-code}

Sometimes, you wish to type-check only part of your program.
You might focus on the most mission-critical or error-prone part of your
code.  When you start to use a checker, you may not wish to annotate
your entire program right away.
% Not having source code is *not* a reason.
You may not have
enough knowledge to annotate poorly-documented libraries that your program uses.

If annotated code uses unannotated code, then the checker may issue
warnings.  For example, the Nullness Checker (Chapter~\ref{nullness-checker}) will
warn whenever an unannotated method result is used in a non-null context:

\begin{Verbatim}
  @NonNull myvar = unannotated_method();   // WARNING: unannotated_method may return null
\end{Verbatim}

If the call \emph{can} return null, you should fix the bug in your program by
removing the \refqualclass{checker/nullness/qual}{NonNull} annotation in your own program.

If the library call \emph{never} returns null,
there are several ways to eliminate the compiler warnings.
\begin{enumerate}
\item Annotate \code{unannotated\_method} in full.  This approach provides
  the strongest guarantees, but may require you to annotate additional
  methods that \code{unannotated\_method} calls.  See
  Chapter~\ref{annotating-libraries} for a discussion of how to annotate
  libraries for which you have no source code.
\item Annotate only the signature of \code{unannotated\_method}, and
  suppress warnings in its body.  Two ways to suppress the warnings are via a
  \code{@SuppressWarnings} annotation or by not running the checker on that
  file (see Chapter~\ref{suppressing-warnings}).
\item Suppress all warnings related to uses of \code{unannotated\_method}
  via the \code{skipUses} processor option
  (see Section~\ref{askipuses}).
  Since this can suppress more warnings than you may expect,
  it is usually better to annotate at least the method's signature.  If you
  choose the boundary between the annotated and unannotated code wisely,
  then you only have to annotate the signatures of a limited number of
  classes/methods
  (e.g., the public interface to a library or package).

\end{enumerate}

Chapter~\ref{annotating-libraries} discusses adding annotations to
signatures when you do not have source code available.
Chapter~\ref{suppressing-warnings} discusses suppressing warnings.

\subsectionAndLabel{Declaration annotations}{declaration-annotations-moved}

When a declaration annotation is an alias for a type annotation, then the
Checker Framework may move the annotation before replacing it by the
canonical version. (If the declaration annotation is in an \<org.checkerframework>
package, it is not moved.)

For example,

\begin{Verbatim}
  import android.support.annotation.NonNull;
  ...
  @NonNull Object [] returnsArray();
\end{Verbatim}

\noindent
is treated as if the programmer had written

\begin{Verbatim}
  import org.checkerframework.checker.nullness.qual.NonNull;
  ...
  Object @NonNull [] returnsArray();
\end{Verbatim}

\noindent
because Android's \<@NonNull> annotation is a declaration annotation, which
is understood to apply to the top-level return type of the annotated method.

When possible, you should use type annotations rather than declaration
annotations.

Users who are using old Java 5--7 declaration annotations (for instance,
from the no-longer-supported FindBugs tool) can use annotations in
package \<org.checkerframework.checker.nullness.compatqual> to avoid name
conflicts.  These are available in package
\href{https://search.maven.org/search?q=a:checker-compat-qual}{\<checker-compat-qual>}
on Maven Central.  Once the users are ready to upgrade to Java 8+ type
annotations, those compatibility annotations are no longer necessary.


% LocalWords:  quals skipUses un AskipUses Alint annotationname javac's Awarns
% LocalWords:  Xlint dotequals castNonNull XDTA Formatter jsr subpart
% LocalWords:  unselect checkbox classpath Djsr bak Nullness nullness java lang
% LocalWords:  checkername util myref nulltest html ESC buildfile mynifty Fenum
% LocalWords:  MyNiftyChecker messagekey basetype uncommenting Anomsgtext
% LocalWords:  AskipDefs mypackage jsr308 Djsr308 Makefile PLXCOMP expr
%  LocalWords:  TODO AsuppressWarnings AssumeAssertion AonlyUses AonlyDefs
%  LocalWords:  ing warningkey redundantNullComparison qual proc Decl
%  LocalWords:  lastsinglesuppression classfiles AwarnUnneededSuppressions
%%  LocalWords:  AshowSuppressWarningKeys NullableType NonNullType JUnit's
%%  LocalWords:  PolyNullType MonotonicNonNullType KeyForType NullableDecl
%%  LocalWords:  NonNullDecl PolyNullDecl MonotonicNonNullDecl KeyForDecl
%%  LocalWords:  refactored AassumeAssertionsAreEnabled assertNotNull
%%  LocalWords:  AassumeAssertionsAreDisabled NullnessUtil checkNotNull
%%  LocalWords:  ElementType AuseSafeDefaultsForUnannotatedSourceCode
% LocalWords:  AuseDefaultsForUncheckedCode checkerframework askipuses
%%  LocalWords:  suppresswarnings ArequirePrefixInWarningSuppressions
%%  LocalWords:  assumeassertion askipdefs alint compat substring
% LocalWords:  AcheckPurityAnnotations