Re: [Javapathfinder-user] Symbolic execution problem.

[Corina P. <Cor...@na...>]

The difference between versions comes from the fact that I changed 
manually the min/max values in MinMax.java.

Corina

Taehoon Lee wrote:
>
> 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??
>>>
>>
>>
>
>