#70 Class.cast() method throws an exception when casting array

[Milos Gligoric]

*** platform ***
JPF svn revision: 1849
Java version: java version "1.6.0_16"
Java(TM) SE Runtime Environment (build 1.6.0_16-b01)
Java HotSpot(TM) Server VM (build 14.2-b01, mixed mode)

*** input program ***
class CCA extends CCB implements CCC {
}
class CCB implements CCC {
}
interface CCC {
}

public class ClassCast {
public static void main(String[] args) throws Exception {
Object o = CCC[].class.cast(new CCB[]{});
if (o == null) {
System.out.print("Equals to null");
} else {
System.out.print("Not equals to null");
}
}
}

*** jpf output ***
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.ClassCastException
at java.lang.Class.cast(Class.java:226)
at ClassCast.main(ClassCast.java:11)
...

*** java output ***
Not equals to null

[Milos Gligoric]

JPF and JVM give different results for the attached program

[Anunay kant]

please have a look .

[Anunay kant]

the problem here is in the cast function in the src/classes/java.lang/class.java file in jpf source code.
actually, it was using the following implementation,

public T cast(Object obj){
if(o!=null && !instanceof(o)){

throws new ClassCastException();
}
return (T)o;
}

here ,the instanceof() function is a native function and its implementation certainly is not working properly.
so ,what i did was
I modified the function as

public T cast(Object o){
try{

return (T)o;
}
catch(ClassCastException e){

throw new ClassCastException();
}

}
this ensures that the exception is thrown only when there is actually one as certified by the try and catch clause.

thank you.