[Javapathfinder-user] I can't execute JPF

[Taehoon, L. <ta...@ky...>]

I'can't execute JPF
why I can't execute JPF ??


~/sw/javapathfinder/examples$ java gov.nasa.jpf.JPF Helloworld
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames
Research Center
java.lang.RuntimeException: Unknown or invalid constant type at 364
at org.apache.bcel.generic.LDC.getType(LDC.java:148)
at gov.nasa.jpf.jvm.bytecode.LDC_W.setPeer(LDC_W.java:47)
at gov.nasa.jpf.jvm.bytecode.Instruction.init(Instruction.java:194)
at gov.nasa.jpf.jvm.bytecode.Instruction.create(Instruction.java:145)
at gov.nasa.jpf.jvm.MethodInfo.loadCode(MethodInfo.java:623)
at gov.nasa.jpf.jvm.MethodInfo.<init>(MethodInfo.java:183)
at gov.nasa.jpf.jvm.MethodInfo.newInstance(MethodInfo.java:257)
at gov.nasa.jpf.jvm.ClassInfo.loadMethods(ClassInfo.java:1167)
at gov.nasa.jpf.jvm.ClassInfo.<init>(ClassInfo.java:252)
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:349)
at gov.nasa.jpf.jvm.JVM.loadStartupClasses(JVM.java:1269)
at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:279)
at gov.nasa.jpf.JPF.run(JPF.java:248)
at gov.nasa.jpf.JPF.main(JPF.java:198)
java.lang.StringIndexOutOfBoundsException: String index out of range: -3
at java.lang.String.substring(String.java:1768)
at java.lang.String.substring(String.java:1735)
at gov.nasa.jpf.jvm.bytecode.Instruction.create(Instruction.java:155)
at gov.nasa.jpf.jvm.MethodInfo.loadCode(MethodInfo.java:623)
at gov.nasa.jpf.jvm.MethodInfo.<init>(MethodInfo.java:183)
at gov.nasa.jpf.jvm.MethodInfo.newInstance(MethodInfo.java:257)
at gov.nasa.jpf.jvm.ClassInfo.loadMethods(ClassInfo.java:1167)
at gov.nasa.jpf.jvm.ClassInfo.<init>(ClassInfo.java:252)
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:349)
at gov.nasa.jpf.jvm.JVM.loadStartupClasses(JVM.java:1269)
at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:279)
at gov.nasa.jpf.JPF.run(JPF.java:248)
at gov.nasa.jpf.JPF.main(JPF.java:198)