-
Notifications
You must be signed in to change notification settings - Fork 348
/
introduction.tex
1686 lines (1423 loc) · 73.3 KB
/
introduction.tex
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
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\htmlhr
\chapterAndLabel{Introduction}{introduction}
The Checker Framework enhances Java's type system to make it more powerful
and useful.
This lets software developers detect and
prevent errors in their Java programs.
A ``checker'' is a compile-time tool that warns you about certain errors or gives you a
guarantee that those errors do not occur.
The Checker Framework comes with checkers for specific types of errors:
\begin{enumerate}
% If you update this list, also update the list in advanced-features.tex .
\item
\ahrefloc{nullness-checker}{Nullness Checker} for null pointer errors
(see \chapterpageref{nullness-checker})
\item
\ahrefloc{initialization-checker}{Initialization Checker} to ensure all
\<@NonNull> fields are set in the constructor (see
\chapterpageref{initialization-checker})
\item
\ahrefloc{map-key-checker}{Map Key Checker} to track which values are
keys in a map (see \chapterpageref{map-key-checker})
\item
\ahrefloc{optional-checker}{Optional Checker} for errors in using the
\sunjavadoc{java.base/java/util/Optional.html}{Optional} type (see
\chapterpageref{optional-checker})
\item
\ahrefloc{interning-checker}{Interning Checker} for errors in equality
testing and interning (see \chapterpageref{interning-checker})
\item
\ahrefloc{called-methods-checker}{Called Methods Checker} for
the builder pattern (see \chapterpageref{called-methods-checker})
\item
\ahrefloc{resource-leak-checker}{Resource Leak Checker} for ensuring that resources are disposed of properly
(see \chapterpageref{resource-leak-checker})
\item
\ahrefloc{fenum-checker}{Fake Enum Checker} to allow type-safe fake enum
patterns and type aliases or typedefs (see \chapterpageref{fenum-checker})
\item
\ahrefloc{tainting-checker}{Tainting Checker} for trust and security errors
(see \chapterpageref{tainting-checker})
\item
\ahrefloc{lock-checker}{Lock Checker} for concurrency and lock errors
(see \chapterpageref{lock-checker})
\item
\ahrefloc{index-checker}{Index Checker} for array accesses
(see \chapterpageref{index-checker})
\item
\ahrefloc{regex-checker}{Regex Checker} to prevent use of syntactically
invalid regular expressions (see \chapterpageref{regex-checker})
\item
\ahrefloc{formatter-checker}{Format String Checker} to ensure that format
strings have the right number and type of \<\%> directives (see
\chapterpageref{formatter-checker})
\item
\ahrefloc{i18n-formatter-checker}{Internationalization Format String Checker}
to ensure that i18n format strings have the right number and type of
\<\{\}> directives (see \chapterpageref{i18n-formatter-checker})
\item
\ahrefloc{propkey-checker}{Property File Checker} to ensure that valid
keys are used for property files and resource bundles (see
\chapterpageref{propkey-checker})
\item
\ahrefloc{i18n-checker}{Internationalization Checker} to
ensure that code is properly internationalized (see
\chapterpageref{i18n-checker})
% The Compiler Message Key Checker is neither here nor in the advanced
% type system features chapter because it is really meant for
% Checker Framework developers and as sample code, and is not meant
% for Checker Framework users at large.
\item
\ahrefloc{signature-checker}{Signature String Checker} to ensure that the
string representation of a type is properly used, for example in
\<Class.forName> (see \chapterpageref{signature-checker})
\item
\ahrefloc{guieffect-checker}{GUI Effect Checker} to ensure that non-GUI
threads do not access the UI, which would crash the application
(see \chapterpageref{guieffect-checker})
\item
\ahrefloc{units-checker}{Units Checker} to ensure operations are
performed on correct units of measurement
(see \chapterpageref{units-checker})
\item
\ahrefloc{signedness-checker}{Signedness Checker} to
ensure unsigned and signed values are not mixed
(see \chapterpageref{signedness-checker})
\item
\ahrefloc{purity-checker}{Purity Checker} to identify whether
methods have side effects (see \chapterpageref{purity-checker})
\item
\ahrefloc{constant-value-checker}{Constant Value Checker} to determine
whether an expression's value can be known at compile time
(see \chapterpageref{constant-value-checker})
\item
\ahrefloc{reflection-resolution}{Reflection Checker} to determine
whether an expression's value (of type \<Method> or \<Class>) can be known at compile time
(see \chapterpageref{reflection-resolution})
\item
\ahrefloc{initialized-fields-checker}{Initialized Fields Checker} to ensure all
fields are set in the constructor (see
\chapterpageref{initialization-checker})
\item
\ahrefloc{aliasing-checker}{Aliasing Checker} to identify whether
expressions have aliases (see \chapterpageref{aliasing-checker})
\item
\ahrefloc{must-call-checker}{Must Call Checker} to over-approximate the
methods that should be called on an object before it is de-allocated (see \chapterpageref{must-call-checker})
\item
\ahrefloc{subtyping-checker}{Subtyping Checker} for customized checking without
writing any code (see \chapterpageref{subtyping-checker})
% \item
% \ahrefloc{typestate-checker}{Typestate checker} to ensure operations are
% performed on objects that are in the right state, such as only opened
% files being read (see \chapterpageref{typestate-checker})
\item
\ahrefloc{third-party-checkers}{Third-party checkers} that are distributed
separately from the Checker Framework
(see \chapterpageref{third-party-checkers})
\end{enumerate}
\noindent
These checkers are easy to use and are invoked as arguments to \<javac>.
The Checker Framework also enables you to write new checkers of your
own; see Chapters~\ref{subtyping-checker} and~\ref{creating-a-checker}.
\sectionAndLabel{How to read this manual}{how-to-read-this-manual}
If you wish to get started using some particular type system from the list
above, then the most effective way to read this manual is:
\begin{itemize}
\item
Read all of the introductory material
(Chapters~\ref{introduction}--\ref{using-a-checker}).
\item
Read just one of the descriptions of a particular type system and its
checker (Chapters~\ref{nullness-checker}--\ref{third-party-checkers}).
\item
Skim the advanced material that will enable you to make more effective
use of a type system
(Chapters~\ref{polymorphism}--\ref{troubleshooting}), so that you will
know what is available and can find it later. Skip
Chapter~\ref{creating-a-checker} on creating a new checker.
\end{itemize}
\sectionAndLabel{How it works: Pluggable types}{pluggable-types}
Java's built-in type-checker finds and prevents many errors --- but it
doesn't find and prevent \emph{enough} errors. The Checker Framework lets you
define new type systems and run them as a plug-in to the javac compiler. Your
code stays completely backward-compatible: your code compiles with any
Java compiler, it runs on any JVM, and your coworkers don't have to use the
enhanced type system if they don't want to. You can check part of
your program, or the whole thing. Type inference tools exist to help you annotate your
code; see Section~\ref{type-inference}.
Most programmers will use type systems created by other people, such as
those listed at the start of the introduction (\chapterpageref{introduction}).
Some people, called ``type system designers'', create new type systems
(\chapterpageref{creating-a-checker}).
The Checker Framework is useful both to programmers who
wish to write error-free code, and to type system designers who wish to
evaluate and deploy their type systems.
This document uses the terms ``checker'' and ``type-checking compiler
plugin'' as synonyms.
\sectionAndLabel{Installation}{installation}
This section describes how to install the Checker Framework.
\begin{itemize}
\item
If you use a build system that automatically downloads dependencies,
such as Gradle or Maven, \textbf{no installation is necessary}; just see
\chapterpageref{external-tools}.
\item
If you wish to try the Checker Framework without installing it, use the
\href{http://eisop.uwaterloo.ca/live/}{Checker Framework Live Demo} webpage.
\item
This section describes how to install the Checker Framework from its
distribution. The Checker Framework release contains everything that you
need, both to run checkers and to write your own checkers.
\item
Alternately, you can build the latest development version from source
(Section~\refwithpage{build-source}).
\end{itemize}
\textbf{Requirement:}
You must have a JDK (version 8 or later) installed.
The installation process has two required steps and one
optional step.
\begin{enumerate}
\item
Download the Checker Framework distribution:
%BEGIN LATEX
\\
%END LATEX
\url{https://checkerframework.org/checker-framework-3.38.0.zip}
\item
Unzip it to create a \code{checker-framework-\ReleaseVersion{}} directory.
\item
\label{installation-configure-step}%
Configure your IDE, build system, or command shell to include the Checker
Framework on the classpath. Choose the appropriate section of
Chapter~\ref{external-tools}.
\end{enumerate}
Now you are ready to start using the checkers.
We recommend that you work through the
\ahreforurl{https://checkerframework.org/tutorial/}{Checker
Framework tutorial}, which demonstrates the Nullness, Regex, and Tainting Checkers.
Section~\ref{example-use} walks you through a simple example. More detailed
instructions for using a checker appear in Chapter~\ref{using-a-checker}.
\label{version-number}
The Checker Framework is released on a monthly schedule. The minor version
(the middle number in the version number) is incremented if there are any
incompatibilities
% Sometimes, we permit trivial incompatibilities, or ones that are unlikely
% to affect users, without changing the minor version.
with the previous version, including in user-visible
behavior or in methods that a checker implementation might call.
\sectionAndLabel{Example use: detecting a null pointer bug}{example-use}
This section gives a very simple example of running the Checker Framework.
There is also a \ahreforurl{https://checkerframework.org/tutorial/}{tutorial}
that you can work along with.
Let's consider this very simple Java class. The local variable \<ref>'s type is
annotated as \refqualclass{checker/nullness/qual}{NonNull}, indicating that \<ref> must be a reference to a
non-null object. Save the file as \<GetStarted.java>.
\begin{Verbatim}
import org.checkerframework.checker.nullness.qual.*;
public class GetStarted {
void sample() {
@NonNull Object ref = new Object();
}
}
\end{Verbatim}
If you run the Nullness Checker (Chapter~\ref{nullness-checker}), the
compilation completes without any errors.
Now, introduce an error. Modify \<ref>'s assignment to:
\begin{alltt}
@NonNull Object ref = \textbf{null};
\end{alltt}
If you run the Nullness Checker again, it emits
the following error:
\begin{Verbatim}
GetStarted.java:5: incompatible types.
found : @Nullable <nulltype>
required: @NonNull Object
@NonNull Object ref = null;
^
1 error
\end{Verbatim}
This is a trivially simple example. Even an unsound bug-finding tool like
SpotBugs or Error Prone could have detected this bug. The
Checker Framework's analysis is more powerful than those tools and detects
more code defects than they do.
Type qualifiers such as \<@NonNull> are permitted anywhere
that you can write a type, including generics and casts; see
Section~\ref{writing-annotations}. Here are some examples:
\begin{alltt}
\underline{@Interned} String intern() \ttlcb{} ... \ttrcb{} // return value
int compareTo(\underline{@NonNull} String other) \ttlcb{} ... \ttrcb{} // parameter
\underline{@NonNull} List<\underline{@Interned} String> messages; // non-null list of interned Strings
\end{alltt}
\htmlhr
\chapterAndLabel{Using a checker}{using-a-checker}
A pluggable type-checker enables you to detect certain bugs in your code,
or to prove that they are not present. The verification happens at compile
time.
Finding bugs, or verifying their absence, with a checker is a two-step process, whose steps are
described in Sections~\ref{writing-annotations} and~\ref{running}.
\begin{enumerate}
\item The programmer writes annotations, such as \refqualclass{checker/nullness/qual}{NonNull} and
\refqualclass{checker/interning/qual}{Interned}, that specify additional information about Java types.
(Or, the programmer uses an inference tool to automatically infer
annotations that are consistent with their code: see Section~\ref{type-inference}.)
It is possible to annotate only part of your code: see
Section~\ref{unannotated-code}.
\item The checker reports whether the program contains any erroneous code
--- that is, code that is inconsistent with the annotations.
\end{enumerate}
This chapter is structured as follows:
\begin{itemize}
\item Section~\ref{writing-annotations}: How to write annotations
\item Section~\ref{running}: How to run a checker
\item Section~\ref{checker-guarantees}: What the checker guarantees
\item Section~\ref{tips-about-writing-annotations}: Tips about writing annotations
\end{itemize}
Additional topics that apply to all checkers are covered later in the manual:
\begin{itemize}
\item Chapter~\ref{advanced-type-system-features}: Advanced type system features
\item Chapter~\ref{suppressing-warnings}: Suppressing warnings
\item Chapter~\ref{annotating-libraries}: Annotating libraries
\item Chapter~\ref{creating-a-checker}: How to create a new checker
\item Chapter~\ref{external-tools}: Integration with external tools
\end{itemize}
There is a
\ahreforurl{https://checkerframework.org/tutorial/}{tutorial}
that walks you through using the Checker Framework on the
command line.
% The annotations have to be on your classpath even when you are not using
% the -processor, because of the existence of the import statement for
% the annotations.
\sectionAndLabel{Where to write type annotations}{writing-annotations}
You may write a type annotation immediately before any
use of a type, including in generics and casts. Because array levels are
types and receivers have types, you can also write type annotations on
them. Here are a few examples of type annotations:
%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{alltt}
\underline{@Interned} String intern() \ttlcb{} ... \ttrcb{} // return value
int compareTo(\underline{@NonNull} String other) \ttlcb{} ... \ttrcb{} // parameter
String toString(\underline{@Tainted} MyClass this) \ttlcb{} ... \ttrcb{} // receiver ("this" parameter)
\underline{@NonNull} List<\underline{@Interned} String> messages; // generics: non-null list of interned Strings
\underline{@Interned} String \underline{@NonNull} [] messages; // arrays: non-null array of interned Strings
myDate = (\underline{@Initialized} Date) beingConstructed; // cast
\end{alltt}
%BEGIN LATEX
\end{smaller}
%END LATEX
You only need to write type annotations on method signatures, fields, and some type arguments.
Most annotations within method bodies are inferred for you; for more details,
see Section~\ref{type-refinement}.
The Java Language Specification also defines
declaration annotations, such as \<@Deprecated> and \<@Override>, which apply
to a class, method, or field but do not apply to the method's return type
or the field's type. They should be written on their own line in the
source code, before the method's signature.
\sectionAndLabel{Running a checker}{running}
To run a checker, run the compiler \code{javac} as usual,
but either pass the \code{-processor \emph{plugin\_class}} command-line
option, or use auto-discovery as described in
Section~\ref{checker-auto-discovery}.
(If your project already uses auto-discovery for some annotation processor,
such as AutoValue, then you should use auto-discovery.)
Two concretes example of using \code{-processor} to run the Nullness Checker are
\begin{Verbatim}
javac -processor nullness MyFile.java
javac -processor org.checkerframework.checker.nullness.NullnessChecker MyFile.java
\end{Verbatim}
\noindent
where \<javac> is as specified in Section~\ref{javac-wrapper}.
You can also run a checker from within your favorite IDE or build system. See
Chapter~\ref{external-tools} for details about build tools such as
Ant (Section~\ref{ant-task}),
Buck (Section~\ref{buck}),
Bazel (Section~\ref{bazel}),
Gradle (Section~\ref{gradle}),
Maven (Section~\ref{maven}), and
sbt (Section~\ref{sbt});
IDEs such as
Eclipse (Section~\ref{eclipse}),
IntelliJ IDEA (Section~\ref{intellij}),
NetBeans (Section~\ref{netbeans}),
and
tIDE (Section~\ref{tide});
and about customizing other IDEs and build tools.
The checker is run on only the Java files that javac compiles.
This includes all Java files specified on the command line and those
created by another annotation processor. It may also include other of
your Java files, if they are more recent than the corresponding \code{.class} file.
Even when the checker does not analyze a class (say, the class was
already compiled, or source code is not available), it does check
the \emph{uses} of those classes in the source code being compiled.
Type-checking works modularly and intraprocedurally: when verifying a
method, it examines only the signature (including annotations) of other
methods, not their implementations. When analyzing a variable use, it
relies on the type of the variable, not any dataflow outside the current
method that produced the value.
After you compile your code while running a checker, the resulting
\<.class> and \<.jar> files can be used for pluggable type-checking of client code.
If you compile code without the \code{-processor}
command-line option, no checking of the type
annotations is performed. Furthermore, only explicitly-written annotations
are written to the \<.class> file; defaulted annotations are not, and this
will interfere with type-checking of clients that use your code.
Therefore, to create
\<.class> files that will be distributed or compiled against, you should run the
type-checkers for all the annotations that you have written.
\subsectionAndLabel{Using annotated libraries}{annotated-libraries-using}
When your code uses a library that is not currently being compiled, the
Checker Framework looks up the library's annotations in its class files or
in a stub file.
Some projects are already distributed with type annotations by their
maintainers, so you do not need to do anything special.
An example is all the libraries in \url{https://github.com/plume-lib/}.
Over time, this should become more common.
For some other libraries, the Checker Framework developers have provided an
annotated version of the library, either as a stub file or as compiled class files.
(If some library is not available in either of these forms,
you can contribute by annotating it, which will
help you and all other Checker Framework users; see
\chapterpageref{annotating-libraries}.)
Some stub files are used automatically by a checker, without any action on
your part. For others, you must pass the \<-Astubs=...> command-line argument.
As a special case, if an \<.astub> file appears in
\<checker/resources/>, then pass the command-line option
use \<-Astubs=checker.jar/\emph{stubfilename.astub}>.
The ``\<checker.jar>'' should be literal --- don't provide a path.
This special syntax only works for ``\<checker.jar>''.
%% There aren't any such libraries at the moment.
% (Examples of such libraries are:
% % This list appears here to make it searchable/discoverable.
% ...
% .)
The annotated libraries that are provided as class files appear in
\href{https://search.maven.org/search?q=org.checkerframework.annotatedlib}{the
\<org.checkerframework.annotatedlib> group in the Maven Central Repository}.
The annotated library has \emph{identical} behavior to the upstream,
unannotated version; the source code is identical other than added
annotations.
%
(Some of the annotated libraries are
% This list appears here to make it searchable/discoverable.
bcel,
commons-csv,
commons-io,
guava,
and
java-getopt.)
To use an annotated library:
\begin{itemize}
\item
If your project stores \<.jar> files locally, then
\href{https://search.maven.org/search?q=org.checkerframework.annotatedlib}{download
the \<.jar> file from the Maven Central Repository}.
\item
If your project manages dependencies using a tool such as Gradle or Maven,
then update your buildfile to use the \<org.checkerframework.annotatedlib>
group. For example, in \<build.gradle>, change
\begin{Verbatim}
api group: 'org.apache.bcel', name: 'bcel', version: '6.3.1'
api group: 'commons-io', name: 'commans-io', version: '2.8'
\end{Verbatim}
\noindent
to
\begin{Verbatim}
api group: 'org.checkerframework.annotatedlib', name: 'bcel', version: '6.3.1'
api group: 'org.checkerframework.annotatedlib', name: 'commons-io', version: '2.8.0.1'
\end{Verbatim}
\noindent
Usually use the same version number. (Sometimes you will use a slightly larger
number, if the Checker Framework developers have improved the type
annotations since the last release by the upstream maintainers.) If a
newer version of the upstream library is available but that version is not
available in \<org.checkerframework.annotatedlib>, then
\ahrefloc{reporting-bugs}{open an issue} requesting that the
\<org.checkerframework.annotatedlib> version be updated.
\end{itemize}
%% This is for paranoid users.
% During type-checking, you should use the
% annotated version of the library to improve type-checking results (to issue
% fewer false positive warnings). When doing ordinary compilation or while
% running your code, you can use either the annotated library or the regular
% distributed version of the library --- they behave identically.
There is one special case. If an \<.astub> file is shipped with the
Checker Framework in \<checker/resources/>, then you can
use \<-Astubs=checker.jar/\emph{stubfilename.astub}>.
The ``\<checker.jar>'' should be literal --- don't provide a path.
(This special syntax only works for ``\<checker.jar>''.)
\subsectionAndLabel{Summary of command-line options}{checker-options}
You can pass command-line arguments to a checker via \<javac>'s standard \<-A>
option (``\<A>'' stands for ``annotation''). All of the distributed
checkers support the following command-line options.
Each checker may support additional command-line options; see the checker's
documentation.
To pass an option to only a particular checker,
prefix the option with the canonical or simple name
of a checker, followed by an underscore ``\<\_>''.
% For the implementation, see SourceChecker.OPTION_SEPARATOR.
Such an option will apply only to a checker with that name or any subclass of that checker.
For example, you can use
\begin{Verbatim}
-ANullnessChecker_lint=redundantNullComparison
-Aorg.checkerframework.checker.guieffect.GuiEffectChecker_lint=debugSpew
\end{Verbatim}
\noindent
to pass different lint options to the Nullness and GUI Effect Checkers. A
downside is that, in this example, the Nullness Checker will issue a
``The following options were not recognized by any processor'' warning
about the second option and the GUI Effect Checker will issue a
``The following options were not recognized by any processor'' warning
about the first option.
% This list should be kept in sync with file
% framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
Unsound checking: ignore some errors
\begin{itemize}
\item \<-AsuppressWarnings>
Suppress all errors and warnings matching the given key; see
Section~\ref{suppresswarnings-command-line}.
\item \<-AskipUses>, \<-AonlyUses>
Suppress all errors and warnings at all uses of a given class --- or at all
uses except those of a given class. See Section~\ref{askipuses}.
\item \<-AskipDefs>, \<-AonlyDefs>
Suppress all errors and warnings within the definition of a given class
--- or everywhere except within the definition of a given class. See
Section~\ref{askipdefs}.
\item \<-AassumeSideEffectFree>, \<-AassumeDeterministic>, \<-AassumePure>
Unsoundly assume that every method is side-effect-free, deterministic, or
both; see
Section~\ref{type-refinement-purity}.
\item \<-AassumeAssertionsAreEnabled>, \<-AassumeAssertionsAreDisabled>
Whether to assume that assertions are enabled or disabled; see Section~\ref{type-refinement-assertions}.
\item \<-AignoreRangeOverflow>
Ignore the possibility of overflow for range annotations such as
\<@IntRange>; see Section~\ref{value-checker-overflow}.
\item \<-Awarns>
Treat checker errors as warnings. If you use this, you may wish to also
supply \code{-Xmaxwarns 10000}, because by default \<javac> prints at
most 100 warnings. If you use this, don't supply \code{-Werror},
which is a javac argument to halt compilation if a warning is issued.
\item \<-AignoreInvalidAnnotationLocations>
Ignore annotations in bytecode that have invalid annotation locations.
\end{itemize}
\label{unsound-by-default}
More sound (strict) checking: enable errors that are disabled by default
\begin{itemize}
\item \<-AcheckPurityAnnotations>
Check the bodies of methods marked
\refqualclass{dataflow/qual}{SideEffectFree},
\refqualclass{dataflow/qual}{Deterministic},
and \refqualclass{dataflow/qual}{Pure}
to ensure the method satisfies the annotation. By default,
the Checker Framework unsoundly trusts the method annotation. See
Section~\ref{type-refinement-purity}.
\item \<-AinvariantArrays>
Make array subtyping invariant; that is, two arrays are subtypes of one
another only if they have exactly the same element type. By default,
the Checker Framework unsoundly permits covariant array subtyping, just
as Java does. See Section~\ref{invariant-arrays}.
\item \<-AcheckCastElementType>
In a cast, require that parameterized type arguments and array elements
are the same. By default, the Checker Framework unsoundly permits them
to differ, just as Java does. See Section~\ref{covariant-type-parameters}
and Section~\ref{invariant-arrays}.
\item \<-AuseConservativeDefaultsForUncheckedCode>
Enables conservative defaults, and suppresses all type-checking warnings,
in unchecked code. Takes arguments ``source,bytecode''.
``-source,-bytecode'' is the (unsound) default setting.
\begin{itemize}
\item
``bytecode'' specifies
whether the checker should apply conservative defaults to
bytecode (that is, to already-compiled libraries); see
Section~\ref{defaults-classfile}.
\item
Outside the scope of any relevant
\refqualclass{framework/qual}{AnnotatedFor} annotation, ``source'' specifies whether conservative
default annotations are applied to source code and suppress all type-checking warnings; see
Section~\ref{compiling-libraries}.
\end{itemize}
\item \<-AconcurrentSemantics>
Whether to assume concurrent semantics (field values may change at any
time) or sequential semantics; see Section~\ref{faq-concurrency}.
\item \<-AconservativeUninferredTypeArguments>
Whether an error should be issued if type arguments could not be inferred and
whether method type arguments that could not be inferred should use
conservative defaults.
By default, such type arguments are (largely) ignored in later
checks.
Passing this option uses a conservative value instead.
See \href{https://github.com/typetools/checker-framework/issues/979}{Issue
979}.
\item \<-AignoreRawTypeArguments=false>
Do not ignore subtype tests for type arguments that were inferred for a
raw type. Must also use \<-AconservativeUninferredTypeArguments>. See
Section~\ref{generics-raw-types}.
\item \<-processor org.checkerframework.common.initializedfields.InitializedFieldsChecker,...>
Ensure that all fields are initialized by the constructor. See
\chapterpageref{initialized-fields-checker}.
\end{itemize}
Type-checking modes: enable/disable functionality
\begin{itemize}
\item \<-Alint>
Enable or disable optional checks; see Section~\ref{lint-options}.
\item \<-AwarnRedundantAnnotations>
Warn about redundant annotations.
A warning is issued if an explicitly written annotation
is the same as the default annotation for that location.
This feature does not warn about all redundant annotations, only some.
\item \<-AsuggestPureMethods>
Suggest methods that could be marked
\refqualclass{dataflow/qual}{SideEffectFree},
\refqualclass{dataflow/qual}{Deterministic},
or \refqualclass{dataflow/qual}{Pure}; see
Section~\ref{type-refinement-purity}.
\item \<-AresolveReflection>
Determine the target of reflective calls, and perform more precise
type-checking based on that information; see
Chapter~\ref{reflection-resolution}. \<-AresolveReflection=debug> causes
debugging information to be output.
\item \<-Ainfer=\emph{outputformat}>
Output suggested annotations for method signatures and fields.
These annotations may reduce the number of type-checking
errors when running type-checking in the future; see
Section~\ref{whole-program-inference}.
Using \<-Ainfer=jaifs> produces \<.jaif> files.
Using \<-Ainfer=stubs> produces \<.astub> files.
Using \<-Ainfer=ajava> produces \<.ajava> files.
You must also supply \<-Awarns>, or the inference output may be incomplete.
\item \<-AinferOutputOriginal>
When outputting \<.ajava> files when running with \<-Ainfer=ajava>,
also output a copy of the original file with no inferred annotations,
but with the formatting of a \<.ajava> file, to permit use of \<diff>
to view the inferred annotations. Must be combined with \<-Ainfer=ajava>.
\item \<-AshowSuppressWarningsStrings>
With each warning, show all possible strings to suppress that warning.
\item \<-AwarnUnneededSuppressions>
Issue a warning if a \<@SuppressWarnings> did not suppress a warning
issued by the checker. This only warns about
\<@SuppressWarnings> strings that contain a checker name
(for syntax, Section~\ref{suppresswarnings-annotation-syntax}). The
\<-ArequirePrefixInWarningSuppressions> command-line argument ensures
that all \<@SuppressWarnings> strings contain a checker name.
An \<unneeded.suppression> warning can be suppressed only by
\<@SuppressWarnings("unneeded.suppression")>
or \<@SuppressWarnings("\emph{checkername}:unneeded.suppression")>,
not by \<@SuppressWarnings("\emph{checkername}")>.
\item \<-AwarnUnneededSuppressionsExceptions=\emph{regex}> disables
\<-AwarnUnneededSuppressions> for \<@SuppressWarnings> strings that
contain a match for the regular expression. Most users don't need this.
\item \<-ArequirePrefixInWarningSuppressions>
Require that the string in a warning suppression annotation begin with a checker
name. Otherwise, the suppress warning annotation does not
suppress any warnings. For example, if this command-line option is
supplied, then \<@SuppressWarnings("assignment")> has no effect, but
\<@SuppressWarnings("nullness:assignment")> does.
\item \<-AshowPrefixInWarningMessages>
When issuing an error or warning, prefix the warning suppression key by
the checker name. For instance, output ``error: [nullness:assignment]
...'' instead of ``error: [assignment]''. This makes it easy to tell,
from the suppression key only, which checker issued the error or warning.
\end{itemize}
Partially-annotated libraries
\begin{itemize}
% \item \<-AprintUnannotatedMethods>
% List library methods that need to be annotated; see
% Section~\ref{annotating-libraries}.
\item \<-Astubs>
List of stub files or directories; see Section~\ref{stub-using}.
\item
\<-AstubWarnIfNotFound>,
\<-AstubNoWarnIfNotFound>,
\<-AstubWarnIfNotFoundIgnoresClasses>,
%% Uncomment when https://tinyurl.com/cfissue/2759 is fixed.
% \<-AstubWarnIfOverwritesBytecode>,
\<-AstubWarnIfRedundantWithBytecode>,
\<-AstubWarnNote>
Warn about problems with stub files; see Section~\ref{stub-troubleshooting}.
\item \<-AmergeStubsWithSource>
If both a stub file and a source file for a class are available, trust
both and use the greatest lower bound of their annotations. The default
behavior (without this flag) is to ignore types from the stub file if
source is available. See Section~\ref{stub-multiple-specifications}.
% note to maintainers: GLB of the two types was chosen to support
% using this flag in combination with \<-Ainfer=stubs>.
% This item is repeated above:
\item \<-AuseConservativeDefaultsForUncheckedCode=source>
Outside the scope of any relevant
\refqualclass{framework/qual}{AnnotatedFor} annotation, use conservative
default annotations and suppress all type-checking warnings; see
Section~\ref{compiling-libraries}.
\end{itemize}
Debugging
\begin{itemize}
\item
\<-AprintAllQualifiers>,
\<-AprintVerboseGenerics>,
\<-Anomsgtext>,
\<-AdumpOnErrors>
Amount of detail in messages; see Section~\ref{creating-debugging-options-detail}.
\item
\<-Adetailedmsgtext>
Format of diagnostic messages; see Section~\ref{creating-debugging-options-format}.
\item
\<-Aignorejdkastub>,
\<-ApermitMissingJdk>,
\<-AparseAllJdk>,
\<-AstubDebug>
Stub and JDK libraries; see Section~\ref{creating-debugging-options-libraries}.
\item
\<-Afilenames>,
\<-Ashowchecks>,
\<-AshowInferenceSteps>,
\<-AshowWpiFailedInferences>
Progress tracing; see Section~\ref{creating-debugging-options-progress}.
\item
\<-AoutputArgsToFile>
Output the compiler command-line arguments to a file. Useful when the
command line is generated and executed by a tool, such as a build system.
This produces a standalone command line that can be executed independently
of the tool that generated it (such as a build system).
That command line makes it easier to reproduce, report, and debug issues.
For example, the command line can be modified to enable attaching a debugger.
See Section~\ref{creating-debugging-options-output-args}.
\item
\<-Aflowdotdir>,
\<-Averbosecfg>,
\<-Acfgviz>
Draw a visualization of the CFG (control flow graph); see
Section~\ref{creating-debugging-dataflow-graph}.
\item
\<-AresourceStats>,
\<-AatfDoNotCache>,
\<-AatfCacheSize>
Miscellaneous debugging options; see Section~\ref{creating-debugging-options-misc}.
\item
\<-Aversion>
Print the Checker Framework version.
\item
\<-AprintGitProperties>
Print information about the git repository from which the Checker Framework
was compiled.
\end{itemize}
\noindent
Some checkers support additional options, which are described in that
checker's manual section.
% Search for "@SupportedOptions" in the implementation to find them all.
For example, \<-Aquals> tells
the Subtyping Checker (see Chapter~\ref{subtyping-checker}) and the Fenum Checker
(see Chapter~\ref{fenum-checker}) which annotations to check.
Here are some standard javac command-line options that you may find useful.
Many of them contain ``processor'' or ``proc'', because in javac jargon, a
checker is an ``annotation processor''.
\begin{itemize}
\item \<-processor> Names the checker to be
run; see Sections~\ref{running} and~\ref{shorthand-for-checkers}.
May be a comma-separated list of multiple checkers. Note that javac
stops processing an indeterminate time after detecting an error. When
providing multiple checkers, if one checker detects any error, subsequent
checkers may not run.
\item \<-processorpath> Indicates where to search for the
checker. This should also contain any classes used by type-checkers,
such as qualifiers used by the Subtyping Checker (see
Section~\ref{subtyping-example}) and classes that define
statically-executable methods used by the Constant Value Checker (see
Section~\ref{constant-value-staticallyexecutable-annotation}).
\item \<-proc:>\{\<none>,\<only>\} Controls whether checking
happens; \<-proc:none>
means to skip checking; \<-proc:only> means to do only
checking, without any subsequent compilation; see
Section~\ref{checker-auto-discovery}.
\item \<-implicit:class> Suppresses warnings about implicitly compiled files
(not named on the command line); see Section~\ref{ant-task}
\item \<-J> Supply an argument to the JVM that is running javac;
for example, \<-J-Xmx2500m> to increase its maximum heap size
\item \<-doe> To ``dump on error'', that is, output a stack trace
whenever a compiler warning/error is produced. Useful when debugging
the compiler or a checker.
\end{itemize}
\subsectionAndLabel{Checker auto-discovery}{checker-auto-discovery}
``Auto-discovery'' makes the \code{javac} compiler always run an
annotation processor, such as a checker
plugin, without explicitly passing the \code{-processor}
command-line option. This can make your command line shorter, and it ensures
that your code is checked even if you forget the command-line option.
If the \<javac> command line specifies any \<-processor> command-line
option, then auto-discovery is disabled. This means that if your project
currently uses auto-discovery, you should use auto-discovery for the
Checker Framework too. (Alternately, if you prefer to use a \<-processor>
command-line argument, you will need to specify all annotation processors,
including ones that used to be auto-discovered.)
\begin{sloppypar}
To enable auto-discovery, place a configuration file named
\code{META-INF/services/javax.annotation.processing.Processor}
in your classpath. The file contains the names of the checkers to
be used, listed one per line. For instance, to run the Nullness Checker and the
Interning Checker automatically, the configuration file should contain:
\end{sloppypar}
%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
org.checkerframework.checker.nullness.NullnessChecker
org.checkerframework.checker.interning.InterningChecker
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX
You can disable this auto-discovery mechanism by passing the
\code{-proc:none} command-line option to \<javac>, which disables all
annotation processing including all pluggable type-checking.
%% Auto-discovering all the distributed checkers by default would be
%% problematic: the nullness and mutability checkers would issue lots of
%% errors for unannotated code, and that would be irritating. So, leave it
%% up to the user to enable auto-discovery.
\subsectionAndLabel{Shorthand for built-in checkers}{shorthand-for-checkers}
% TODO: this feature only works for our javac script, not when using
% the standard javac. Should this be explained?
Ordinarily, javac's \code{-processor} flag requires fully-qualified class names.
When using the Checker Framework javac wrapper (Section~\ref{javac-wrapper}), you may
omit the package name and the \<Checker> suffix.
The following three commands are equivalent:
\begin{alltt}
javac -processor \textbf{org.checkerframework.checker.nullness.NullnessChecker} MyFile.java
javac -processor \textbf{NullnessChecker} MyFile.java
javac -processor \textbf{nullness} MyFile.java
\end{alltt}
This feature also works when multiple checkers are specified.
Their names are separated by commas, with no surrounding space.
For example:
\begin{alltt}
javac -processor NullnessChecker,RegexChecker MyFile.java
javac -processor nullness,regex MyFile.java
\end{alltt}
This feature does not apply to javac \href{https://docs.oracle.com/javase/7/docs/technotes/tools/windows/javac.html#commandlineargfile}{@argfiles}.
\sectionAndLabel{What the checker guarantees}{checker-guarantees}
A checker guarantees two things: type annotations reflect facts about
run-time values, and illegal operations are not performed.
For example, the Nullness Checker (Chapter~\ref{nullness-checker})
guarantees lack of null pointer exceptions (Java \<NullPointerException>).
More precisely, it guarantees
that expressions whose type is annotated with
\refqualclass{checker/nullness/qual}{NonNull} never evaluate to null,
and it forbids other expressions from being dereferenced.
As another example, the Interning Checker (Chapter~\ref{interning-checker})
guarantees that correct equality tests are performed.
More precisely, it guarantees that
every expression whose type is an \refqualclass{checker/interning/qual}{Interned} type
evaluates to an interned value, and it forbids
\<==> on other expressions.
The guarantee holds only if you run the checker on every part of your
program and the checker issues no warnings anywhere in the code.
You can also verify just part of your program.
There are some limitations to the guarantee.
\begin{itemize}
\item
A compiler plugin can check only those parts of your program that you run
it on. If you compile some parts of your program without running the
checker, then there is no guarantee that the entire program satisfies the
property being checked. Some examples of un-checked code are:
\begin{itemize}
\item
Code compiled without the \code{-processor} switch. This includes
external libraries supplied as a \code{.class} file and native methods
(because the implementation is not Java code, it cannot be checked).
\item
Code compiled with the \code{-AskipUses}, \code{-AonlyUses}, \code{-AskipDefs} or \code{-AonlyDefs}
command-line arguments (see Chapter~\ref{suppressing-warnings}).
\item
Dynamically generated code, such as generated by Spring or MyBatis.
Its bytecode is directly generated and run, not compiled by javac and
not visible to the Checker Framework.
% https://github.com/typetools/checker-framework/issues/3139
\end{itemize}
In each of these cases, any \emph{use} of the code is checked --- for
example, a call to a native method must be compatible with any
annotations on the native method's signature.
However, the annotations on the un-checked code are trusted; there is no
verification that the implementation of the native method satisfies the
annotations.
\item
You can suppress warnings, such as via the \code{@SuppressWarnings}
annotation (\chapterpageref{suppressing-warnings}). If you do so
incorrectly, the checker's guarantee no longer holds.
\item
The Checker Framework is, by default, unsound in a few places where a
conservative analysis would issue too many false positive warnings.
These are listed in Section~\ref{unsound-by-default}.
You can supply a command-line argument to make the Checker Framework
sound for each of these cases.
%% This isn't an unsoundness in the Checker Framework: for any type system