Re: [Javapathfinder-user] one question about symbolic execution overloop

[Pasareanu, C. S. (ARC-TI)[S. G. T. INC.] <Cor...@na...>]

the reason is we do not handle Strings yet.

Corina Pasareanu, PhD
http://ase.arc.nasa.gov/people/pcorina/



-----Original Message-----
From: jiangfan shi [mailto:jia...@gm...]
Sent: Wed 1/7/2009 1:28 PM
To: jav...@li...
Subject: [Javapathfinder-user] one question about symbolic execution overloop
 
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

------------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It is the best place to buy or sell services for
just about anything Open Source.
http://p.sf.net/sfu/Xq1LFB
_______________________________________________
Javapathfinder-user mailing list
Jav...@li...
https://lists.sourceforge.net/lists/listinfo/javapathfinder-user