Re: [JPF] jpf-symbc support for Java applets

23 views
Skip to first unread message
Message has been deleted

Corina Pasareanu

unread,
Jun 18, 2013, 2:49:05 PM6/18/13
to java-pa...@googlegroups.com
what is the symbolic method here?

corina


On Mon, Jun 17, 2013 at 6:14 AM, Adrian <adrian.h...@gmail.com> wrote:
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.
 
 

Reply all
Reply to author
Forward
0 new messages