Menu
▾
▴
Re: [Javapathfinder-user] Symbolic execution problem.
|
From: Taehoon L. <ta...@kg...> - 2008-04-03 23:05:58
|
Thank you for your replies.
However, what I want to know is following test input is correct
(y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0
and I think difference between versions is not caused by MinMax.java
Same test input is generated when MinMax.java is reverted to previous
version.
Corina Pasareanu ? ?:
> 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??
>>>>
>>>>
>>>
>>
>
>
> -------------------------------------------------------------------------
> Check out the new SourceForge.net Marketplace.
> It's the best place to buy or sell services for
> just about anything Open Source.
> http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>
>
--
------------------------------------------------------
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...
-------------------------------------------------------
|
