Re: [Javapathfinder-user] Symbolic execution problem.

[Taehoon L. <ta...@kg...>]

Test program is following

------------------------------------------------------------------------------------------------------------ 

import gov.nasa.jpf.symbc.Debug;


public class MyClass1 {
// The method you need tests for
public int myMethod(int x, int y) {
int z = x + y;
if (z > 0) {
z = 1;
} else {
z = z - x;
}
z = x * z;
return z;
}

// The test driver
public static void main(String[] args) {
MyClass1 mc = new MyClass1();
int x = mc.myMethod(1, 2);
Debug.printPC("\nMyClass1.myMethod Path Condition: ");
}
}
------------------------------------------------------------------------------------------------------------- 


I execute it with following options
-------------------------------------------------------------------------------------------------------------- 

+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+vm.classpath=.
+vm.storage.class=
+symbolic.method=myMethod(sym#sym)
+jpf.report.console.finished=
MyClass1
-------------------------------------------------------------------------------------------------------------- 




I have two kind of the problem,
first problem is the number of 2147483647 which is the maxinum number of 
int in general case
however JPF generate some condition which is greater than 2147483647.

second problem, test input is different when version is changed

with revision 794 in svn, I got following test input

====================================================== search started: 
08. 4. 4 ?? 7:28

Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, y_2_SYMINT )

MyClass1.myMethod Path Condition: # = 1
(y_2_SYMINT[-9999] + x_1_SYMINT[10000]) > CONST_0

MyClass1.myMethod Path Condition: # = 1
(y_2_SYMINT[-10000] + x_1_SYMINT[-10000]) <= CONST_0

====================================================== search finished: 
08. 4. 4 ?? 7:28

with revision 795 in svn, I got following test input
====================================================== search started: 
08. 4. 4 ?? 7:31

Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, y_2_SYMINT )

MyClass1.myMethod Path Condition: # = 1
(y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) > CONST_0

MyClass1.myMethod Path Condition: # = 1
(y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0

====================================================== search finished: 
08. 4. 4 ?? 7:31




Corina Pasareanu ? ?:
>
> could you tell us what is the test program?
> why is
>
> 2147483647
>
> not a good number?
>
> Corina
>
> Taehoon Lee wrote:
>> Hi, My name is Taehoon
>>
>> I have two question
>> first, Could you tell me the difference between extension/symbolic and
>> extension/symbc
>>
>> secondly
>>
>> When I execute JPF in Symbolic Execution Mode with following options,
>> ---------------------------------------------------------------------------------- 
>>
>> +vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
>> +vm.classpath=. +vm.storage.class= +symbolic.method=myMethod(sym#sym)
>> +jpf.report.console.finished= MyClass1
>> ---------------------------------------------------------------------------------- 
>>
>>
>> I receive following results
>>
>> ---------------------------------------------------------------------------------- 
>>
>> Execute symbolic INVOKESPECIAL: myMethod2(II)I ( x_1_SYMINT, 
>> y_2_SYMINT )
>>
>> MyClass2.myMethod2 Path Condition: # = 2
>> x_1_SYMINT[2147483647] >= CONST_5 && (y_2_SYMINT[2147483647] +
>> x_1_SYMINT[2147483647]) > CONST_0
>>
>> MyClass2.myMethod2 Path Condition: # = 2
>> x_1_SYMINT[2147483647] < CONST_5 && (y_2_SYMINT[2147483647] +
>> x_1_SYMINT[2147483647]) <= CONST_0
>> ---------------------------------------------------------------------------------- 
>>
>>
>> I think the number 2147483647 is not correct test input data.
>> The JPF which is in subversion repository is unstable??
>>
>
>


-- 
------------------------------------------------------
Taehoon Lee

Ph.D candidate
Department of Computer Science
Kyonggi University
San94-6, Yiui-dong, Yongtong-gu, Suwon-si, 442-760, South Korea
TEL: +82-11-9932-2732
EMAIL: ta...@kg...
-------------------------------------------------------