Cast annotation is not properly generated in the class file

[GoogleCodeExporter]

from whq1238000@gmail.com:

 have found a possible bug in the checker-framework. After compiling with its javac I found the cast (target type 0x47) annotation contains offset which has value 0. It turns out the cast annotation is not properly generated in the class file. 
     Annotation : 0x47000000 (b1 b2 b3 b4). where b1 is 0x47 and b2<<<8 + b3 is the offset. 

The checker I am using is 1.8.10 version and I have attached the source and 
compiled byte code. To be more specific, the problem is when we attach an cast 
annotation to a range of byte code, the offset doesn't  point to the last byte 
code within range. Instead the checker attach the cast annotation to the 
nearest byte code.
    In the example I attached, the getSource() method should put a cast at offset 3 in principle while the checker put it at offset 2. 
   This type of bugs happen in places where we evaluate a non-static method call or get field instructions.For example, in (@Untainted int) x. f and (@Untainted int) x.get(), the cast is by mistake attached to x as opposed to the actual evaluated value of type int.

Original issue reported on code.google.com by mcart...@cs.washington.edu on 12 Mar 2015 at 9:30

Attachments:

• MyTest.java
• MyTest.out