Problems with Mutable

[GoogleCodeExporter]

Trying to use the javari checker (0.0.18):

Two issues, described below
- need some control over which annotation types are implicitly imported
- can't get Mutable to work (which is perhaps just an explanation and 
documentation problem)

------------------

With no annotations added (except nullness ones, in comments, which pass).  
javari reports a problem:

C:\cygwin\home\dcok\eclipseProjects\SMT\src\org\smtlib\SMT.java:168: 
incompatible types.

            Class<?> o = Class.forName(name);
                                      ^
  found   : @Mutable Class<? extends @ReadOnly Object>

  required: @Mutable Class<? extends @Mutable Object>
1 error

However:
This:           Class<? extends /*@Mutable*/ Object> o = Class.forName(name);
(with no imports)

produces

C:\cygwin\home\dcok\eclipseProjects\SMT\src\org\smtlib\SMT.java:168: reference 
to Mutable is ambiguous, both class checkers.javari.quals.Mutable in 
checkers.javari.quals and class checkers.igj.quals.Mutable in 
checkers.igj.quals match
            Class<? extends /*@Mutable*/ Object> o = Class.forName(name);
                               ^
C:\cygwin\home\dcok\eclipseProjects\SMT\src\org\smtlib\SMT.java:168: reference 
to Mutable is ambiguous, both class checkers.javari.quals.Mutable in 
checkers.javari.quals and class checkers.igj.quals.Mutable in 
checkers.igj.quals match
            Class<? extends /*@Mutable*/ Object> o = Class.forName(name);
                               ^
1 error

even though I'm only checking with javari

Adding an explicit: import checkers.javari.quals.Mutable;
does not fix the above (probably because I have to keep the implicit import 
turned on because of the nullness annotations)

Making the commented annotation explicit:           Class<? extends 
/*@checkers.javari.quals.Mutable*/ Object> o = Class.forName(name);

still produces

C:\cygwin\home\dcok\eclipseProjects\SMT\src\org\smtlib\SMT.java:168: 
incompatible types.

            Class<? extends /*@checkers.javari.quals.Mutable*/ Object> o = Class.forName(name);
                                                                                        ^
  found   : @Mutable Class<? extends @ReadOnly Object>

  required: @Mutable Class<? extends @Mutable Object>
1 error

So lets try non-comment annotations:
            Class<? extends @Mutable Object> o = Class.forName(name);

gives a Java syntax error on @Mutable

Original issue reported on code.google.com by c...@frontiernet.net on 21 Aug 2010 at 4:18

[GoogleCodeExporter]

So to be clear, when you specify the ambiguous @Mutable annotation in the 
commented version, the result is what you expect, right? If I understand your 
report correctly, this is likely caused by the "all in" way of using implicit 
imports right now. In that case, the imports could be exposed so the user can 
set which annotations to import. Would that fix your issue?

Original comment by asumu.ta...@gmail.com on 23 Aug 2010 at 4:48

• Changed state: Accepted

[GoogleCodeExporter]

There is the ambiguity - so as you say it would be helpful to have a way to 
control which imports and implicitly imported.

More important however, I could find no way to make Mutable work by 
dis-ambiguating it - Making the annotation fully qualified in the comment form 
did not work
- Writing the annotation in the Java7 form caused a Java syntax error.

Original comment by c...@frontiernet.net on 23 Aug 2010 at 11:55

[GoogleCodeExporter]

I agree that the plugin needs to not import every annotation, but only the
ones relevant to the checker that is being used.

When you said in comment 2 that "Making the annotation fully qualified in
the comment form did not work", do you just mean that the Javari checker
issued a warning in that case?  That would seem to be a problem with either
the Javari checker, or with the annotations that you wrote; in either case,
it has nothing to do with the Eclipse plug-in.  (Or, am I missing something?)

If there are problems with the checker itself, please report them in the
Checker Framework issue tracker rather than here in the Eclipse plugin
checker.  Thanks!

Original comment by michael.ernst@gmail.com on 27 Aug 2010 at 8:07

[GoogleCodeExporter]

The problem with implicit imports has been fixed in the latest version (on the 
update site as 1.0.1). Implicit import paths are now only used for checkers 
that are explicitly selected in the preferences. Thanks for the feedback. 
Marking this as fixed now.

Original comment by asumu.ta...@gmail.com on 27 Aug 2010 at 10:32

• Changed state: Fixed

[GoogleCodeExporter]

This works for me: Windows 64 bit, 1.0.2.  Thanks for the fix.

Original comment by c...@frontiernet.net on 11 Sep 2010 at 1:21