Hi all,
What is the current status of support for applets by jpf (and in particular jpf-symbc)? Note that I don't necessarily mean GUI-based applets, but just Java programs that do not have a main method and instead inherit from the Applet class.
I've realised that an applet cannot be executed directly (due to the lack of a main method, which is fair enough). However, even with a driver program I run into exceptions with jpf-symbc.
Below is a code snippet and the error it produces:
AppletTest.java
import java.applet.Applet;
public class AppletTest extends Applet {
public AppletTest() {
System.out.println("This is an applet.");
}
}
AppletDriver.java
public final class AppletDriver {
public static void main(String[] args) {
AppletTest appTest = new AppletTest();
}
}
AppletTest.jpf
target=AppletDriver
classpath=/the/classpath
#symbolic.method=
listener=gov.nasa.jpf.symbc.SymbolicListener
The output is as follows:
Running Symbolic PathFinder ...
symbolic.dp=choco
symbolic.string_dp_timeout_ms=0
symbolic.string_dp=none
symbolic.choco_time_bound=30000
symbolic.min_int=-1000000
symbolic.max_int=1000000
symbolic.min_double=-8.0
symbolic.max_double=7.0
JavaPathfinder v6.0 (rev 1039) - (C) RIACS/NASA Ames Research Center
====================================================== system under test
application: AppletDriver.java
====================================================== search started: 17/06/13 10:33 PM
[SEVERE] JPF exception, terminating: exception during instructionExecuted() notification
java.lang.AssertionError: can't find caller stackframe for: invokevirtual java.lang.String.length()I
at gov.nasa.jpf.jvm.bytecode.InvokeInstruction.getArgumentValues(InvokeInstruction.java:153)
at gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:236)
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:755)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:2256)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:2197)
at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:781)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1794)
at gov.nasa.jpf.search.Search.forward(Search.java:533)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
at gov.nasa.jpf.JPF.run(JPF.java:618)
at gov.nasa.jpf.JPF.start(JPF.java:190)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:616)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:100)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during instructionExecuted() notification
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:766)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:2256)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:2197)
at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:781)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1794)
at gov.nasa.jpf.search.Search.forward(Search.java:533)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
at gov.nasa.jpf.JPF.run(JPF.java:618)
at gov.nasa.jpf.JPF.start(JPF.java:190)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:616)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:100)
Caused by: java.lang.AssertionError: can't find caller stackframe for: invokevirtual java.lang.String.length()I
at gov.nasa.jpf.jvm.bytecode.InvokeInstruction.getArgumentValues(InvokeInstruction.java:153)
at gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:236)
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:755)
... 14 more
I guess I am confused about the error more than anything else. Why is it failing on java.lang.String.length()? It doesn't normally fail on this method. Is there anyway I can get jpf to output the particular class/method/line number that it is failing at?
Any help would be greatly appreciated!
Thanks,
Adrian
--
---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.