@Interned and autoboxing

[GoogleCodeExporter]

The type checker manual says: "... object creation expressions (using new) are 
never considered @Interned unless they are annotated as such, as in
@Interned Double internedDoubleZero = new @Interned Double(0); "

I would expect that 

@Interned Double internedDoubleZero = new Double(0);

would result in a type checker warning then.  However, the type checker does 
not warn.

Similarly, I would expect a warning when the following method is invoked with 
non-interned values:

boolean method(@Interned Character a, @Interned Character b) {return a==b;}

method(new Character('a'),new Character('a'));  // <== oops, no warning ???
method('ä','ü');                                // dito

What version of the product are you using? On what operating system?

javac 1.7.0-jsr308-1.1.0b on Windows

Original issue reported on code.google.com by ja...@angelikalanger.com on 30 Aug 2010 at 6:34

[GoogleCodeExporter]

My fault.  I used the wrong checker. 

Suggestion for minor improvement of the type checker manual:  
It would help if the various sections such as "Chapter 4  Interning checker" 
would mention the name of the respective checker right away (rather than 
mentioning the checker's name in the very last paragraph).  Similar to the 
JavaDoc where is says: "This annotation is associated with the SoAndSoChecker." 

Still, the following invocations do not trigger warnings although one would 
expect them:

method('ä','ü');  
method(Character.valueOf('a'),'a');

At least a type checker that is delivered as part of the JDK should ideally 
know which values the corresponding compiler/JVM will intern.

Original comment by ja...@angelikalanger.com on 30 Aug 2010 at 7:10

[GoogleCodeExporter]

I made the documentation change you proposed.

> method('ä','ü');  

The checker isn't properly handling the auto-boxing from char to Character.
Thanks for noticing this bug.

> method(Character.valueOf('a'),'a');

This does produce a warning, for me, using the current Checker Framework in
the repository.  I'm not sure why it does not produce a warning for you.

I've changed the title of this issue to be more descriptive.

Original comment by michael.ernst@gmail.com on 30 Aug 2010 at 11:23

• Changed title: @Interned and autoboxing

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 31 Aug 2010 at 4:20

• Changed state: Accepted

[GoogleCodeExporter]

The bugs (to my mind) are:

Autoboxed characters such as 'ä' and 'ü' are accepted as interned by the 
checker although the should not.  Whether they are interned is a jdk specific 
implementation issue; usually they are not interned. Only values in the range 
'\u0000' to '\u007f' are guaranteed to be interned.

Character.valueOf('a') is not considered an interned object by the checker 
although in fact it is interned.  It is the same as an autoboxed 'a' which the 
checker correctly accepts as interned.

Original comment by ja...@angelikalanger.com on 31 Aug 2010 at 6:28

[GoogleCodeExporter]

Thanks for the clarifications.  That helps.
We'll work on these bugs.

Original comment by michael.ernst@gmail.com on 1 Sep 2010 at 6:17