[Checkers] Spaces in commented JSR 308 annotations

Michael Ernst mernst at csail.mit.edu
Tue Jun 10 03:40:42 EDT 2008


Adam-

Thanks for raising these valid concerns.

I am motivated by another concern:  to the greatest extent possible, the
compiler should not reject programs that were legal before.  For example,
existing programs that use "/*@" as a comment marker should still compile.
A few tools that use this prefix are ESC/Java, JML, and Splint; doubtless
there are others that I don't know of.

For example, here is a program containing a JML comment "/*@ pure */".

  /** Test d1 and d2 for non-equality. **/
  /*@ pure */
  boolean ne (double d1, double d2) {
    return d1 != d2;
  }

If javac ignores spaces when deciding whether to ignore the "/*" and "*/",
then it issues a warning because "pure" is not defined as an annotation:

  cannot find symbol
  symbol  : class pure

> Doesn't the compiler know which @ things are annotations and which are
> not (from the classpath)?

If a programmer mistypes an annotation, there should be a compiler error,
just like the one I showed above.  I think it would be worse for the
compiler to silently ignore some annotation comments and process others,
without any indication to the programmer of which is which.


If it would help (and especially if it would make you, or Sung, use the
compiler regularly), we could add an environment variable that you can set
to change the default behavior, so you don't have to type the
-Xspacesincomments argument.  I suppose we could also make the default go
the other way and have a command-line argument and environment variable to
override it.

Thanks for the comments.

                    -Mike



More information about the checkers mailing list