java.lang.RuntimeException: Edge not understood

[Muzammil Shahbaz]

Hi,

When running symbolic execution on a Java class, I am getting this
error trace:

java.lang.RuntimeException: Edge not understood
at
gov.nasa.jpf.symbc.string.translate.TranslateToAutomata2.handleEdge(TranslateToAutomata2.java:
295)
at
gov.nasa.jpf.symbc.string.translate.TranslateToAutomata2.inner_isSat(TranslateToAutomata2.java:
114)
at
gov.nasa.jpf.symbc.string.translate.TranslateToAutomata2.isSat(TranslateToAutomata2.java:
76)
at
gov.nasa.jpf.symbc.string.SymbolicStringConstraintsGeneral.inner_isSatisfiable(SymbolicStringConstraintsGeneral.java:
510)
at
gov.nasa.jpf.symbc.string.SymbolicStringConstraintsGeneral.isSatisfiable(SymbolicStringConstraintsGeneral.java:
345)
at
gov.nasa.jpf.symbc.string.StringPathCondition.simplify(StringPathCondition.java:
121)
at
gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:
286)
at gov.nasa.jpf.symbc.bytecode.IF_ICMPNE.execute(IF_ICMPNE.java:105)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:
2197)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:
2159)
at
gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:
650)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1755)
at gov.nasa.jpf.search.Search.forward(Search.java:492)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
at gov.nasa.jpf.JPF.run(JPF.java:558)
at gov.nasa.jpf.JPF.start(JPF.java:170)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:
39)
at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:
25)
at java.lang.reflect.Method.invoke(Method.java:597)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:99)

The Java class is given here:

public class URIUtil {

public static String getParentURI(String uri) {

if (uri.endsWith("/")) {
uri = uri.substring(0, uri.length() - 2);
}

int index = uri.indexOf("/");
int index2 = uri.lastIndexOf("/");

if (index == index2) {
return " ";
}

return uri.substring(0, uri.lastIndexOf("/"));
}


public static void main(String[] a) {
getParentURI("//");
}
}

The jpf file is here:

....
symbolic.dp=choco
symbolic.string_dp=automata
symbolic.method=se.kth.cid.identity.URIUtil.getParentURI(sym)
#listener = gov.nasa.jpf.symbc.SymbolicListenerClean
listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener
vm.storage.class=nil