Menu
▾
▴
Re: [Javapathfinder-user] Symbolic execution problem.
|
From: Corina P. <Cor...@na...> - 2008-04-04 00:26:20
|
OK -- I added the solver in the new code.
The mixed integer/real constraints still need to be tested.
Corina
Taehoon Lee wrote:
>
> 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
>>
>>
>
>
|
