Relationship between stubs and .java files

[GoogleCodeExporter]

The Checker Framework Manual states:

  The -Astubs argument causes the Checker Framework to read annotations
  from annotated stub classes in preference to the unannotated original
  library classes.

In other words, if A.java is being compiled, and a stub for B exists, and
B.class exists, then the stubs take precedence.

However, the manual does not say which takes precedence between an
annotated stub class and a source file that is being compiled.  For
example, suppose that A.java is being compiled, and a stub for A exists.

Currently, the stub for A is completely ignored.
If this is desired behavior, then it should be documented.

Other reasonable alternatives would be to use the stub, or to merge the
annotations in the stub with those in the .java file.  Either of these
approaches would permit the user to type-check a file that the user is
unable to modify.

For instance, suppose that I want to type-check a program, but my manager
doesn't want to clutter the code with annotations, even in comments.  The
approach of putting annotations in a stub file seems like a good
alternative (it doesn't permit annotation of local variables, but such
annotations are rarely needed), but will not work with the current
behavior.

Original issue reported on code.google.com by michael.ernst@gmail.com on 23 Jun 2010 at 4:30

[GoogleCodeExporter]

Also, whenever the Checker Framework ignores a stub file, it should output
a message to that effect rather than just silently ignoring it, which is
very mysterious to users.

Original comment by michael.ernst@gmail.com on 23 Jun 2010 at 4:40

[GoogleCodeExporter]

Original comment by wdi...@gmail.com on 25 Nov 2013 at 6:37