[Javapathfinder-user] one question about symbolic execution over loop

[jiangfan s. <jia...@gm...>]

Hi, All,

I encountered a problem with the symbolic execution package inside the
jpf. I show the problem with the following example.

I have a code like this:

package jpftest;

public class B {

	void test2(String str1){
		for(int i=0;i<str1.length();i++)
			System.out.println(str1+i);
	}
	public static void main(String args[]){

		B b=new B();
		b.test2("hello");


	}

}

I ran JPF with the following options:

-c ../../../default.properties
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+jpf.listener=gov.nasa.jpf.symbc.HeapSymbolicListener
+symbolic.dp=choco
+symbolic.method=test2(sym)
jpftest.B

I got the outputs from JPF as following:

symbolic.dp=choco
Symbolic Execution Mode
---->Heap Listener
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center


====================================================== system under test
application: jpftest\B.java

====================================================== search started:
09-1-7 下午1:23

Execute symbolic INVOKEVIRTUAL: test2(Ljava/lang/String;)V  ( str1_1_SYMREF )
hello0
hello1
hello2
hello3
hello4
PC # = 0
Heap PC # = 0
Effect is  # = 1
B:this == B:#271
****************************

====================================================== Method Summaries
No path conditions for test2(java.lang.String@272)

====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic Java Path Finder for test2 (Path
Coverage) </h1>
No path conditions for test2(java.lang.String@272)

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       0:00:01
states:             new=2, visited=0, backtracked=1, end=1
search:             maxDepth=1, constraints=0
choice generators:  thread=1, data=1
heap:               gc=2, new=289, free=32
instructions:       2984
max memory:         4MB
loaded code:        classes=68, methods=993

====================================================== search
finished: 09-1-7 下午1:23


The question is that why there is no path condition? I assume for a
"for loop" there should be infinite paths, or with a depth threshold
option there should be some paths. But from the output, I did not see
any path condition.

Did I miss some options to handle the loop specially, or someelse I
should take care of?

Thanks in advance for your help!

Jiangfan