There are some errors in my configuration about symbc, help

48 views
Skip to first unread message

Erik

unread,
Jul 8, 2011, 6:14:05 AM7/8/11
to Java™ Pathfinder
I want to test all paths of a small program. Its source codes are
here :

import java.io.*;

public class InputSymbol
{
public void test() {
int i = 0;
BufferedReader stdin =
new BufferedReader(new InputStreamReader(System.in));

try {
i = Integer.parseInt(stdin.readLine());
} catch (Exception e) {
;
}

if (i >= 100)
assert false: "i>=100";
else if (i <= 50)
assert false: "i<=50";
else
assert false: "50-100";
}

public static void main(String[] argv) {
InputSymbol input = new InputSymbol();
input.test();
}
}

And the configuration is:
vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
# symbolic.method=test(sym#sym)
symbolic.method=test
jpf.listener=gov.nasa.jpf.symbc.SymbolicListener

And errors always happen when I test the program with jpf.
I guess the configuration is not right. But I don't know how to corret
it. plz help me

Eric

unread,
Jul 11, 2011, 9:36:03 PM7/11/11
to Java™ Pathfinder
Anyone around here?

the following is the error-log

$ jpf -c InputSymbol.properties InputSymbol
symbolic.dp=choco
Symbolic Execution Mode
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center


====================================================== system under test
application: InputSymbol.java

====================================================== search started: 7/12/11 9:34 AM
[SEVERE] JPF exception, terminating: exception during instructionExecuted() notification
java.lang.StringIndexOutOfBoundsException: String index out of range: -1
    at java.lang.String.substring(String.java:1949)
    at gov.nasa.jpf.symbc.bytecode.BytecodeUtils.isMethodSymbolic(BytecodeUtils.java:89)
    at gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:195)
    at gov.nasa.jpf.jvm.VMListenerMulticaster.instructionExecuted(VMListenerMulticaster.java:139)
    at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:569)
    at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1687)
    at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:2371)
    at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:506)
    at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1467)
    at gov.nasa.jpf.search.Search.forward(Search.java:403)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:83)
    at gov.nasa.jpf.JPF.run(JPF.java:529)
    at gov.nasa.jpf.JPF.main(JPF.java:161)
Exception in thread "main" ---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during instructionExecuted() notification
    at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:579)
    at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1687)
    at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:2371)
    at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:506)
    at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1467)
    at gov.nasa.jpf.search.Search.forward(Search.java:403)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:83)
    at gov.nasa.jpf.JPF.run(JPF.java:529)
    at gov.nasa.jpf.JPF.main(JPF.java:161)
Caused by: java.lang.StringIndexOutOfBoundsException: String index out of range: -1
    at java.lang.String.substring(String.java:1949)
    at gov.nasa.jpf.symbc.bytecode.BytecodeUtils.isMethodSymbolic(BytecodeUtils.java:89)
    at gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:195)
    at gov.nasa.jpf.jvm.VMListenerMulticaster.instructionExecuted(VMListenerMulticaster.java:139)
    at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:569)
    ... 8 more


need help. Ths

Eric

unread,
Jul 12, 2011, 3:33:52 AM7/12/11
to Java™ Pathfinder
Now I notice the sourecode I got from sourceforge.com was not supported. I'm sorry for inconvenient.
Reply all
Reply to author
Forward
0 new messages