javapathfinder-devel

[Javapathfinder-devel] State seen

[Michal K. <mic...@gm...>]

Hi,

I have the following JUnit test executed under JPF.

public class MathTest {
	@Test
	public void add() {
		System.out.println("add");
		int x = Verify.getInt(1, 2);
	}

	@Test
	public void divide() throws Exception {
		System.out.println("divide");
	}
}

And I'm curious why the second test 'divide' is run twice. Firstly I thought 
it's clear, the 'add' test generates two values in the variable 'x' so the 
division will be invoked twice as well. But later I realized that x is a local 
variable that shouldn't affect the rest of the class. I think the state of VM 
before the division is invoked should be the same in both cases. Am I right or not?

Thanks

Michal

Re: [Javapathfinder-devel] State seen

[Mateusz U. <mat...@gm...>]

Hi,

    I did some debbuging and here what I've got.
> I think the state of VM 
> before the division is invoked should be the same in both cases. Am I right or not?
>   
    Yes you are right the state is the same. I've checked that by adding 
some code into NativePeer.executeMethod() which is invoked for example 
when JPF finds
"System.out.println("divide");". But after learning that, I get 
confused, because I thought if the state has been seen already seen, JPF 
should not execute
any more code on that path. I did some more debugging and that's why it 
executes all the code:
    After printing first "divide" JPF backtracks to "int x = 
Verify.getInt(1, 2); ". And starts to execute this code, execution of 
this code is done in ThreadInfo.executeStep method.
This method executes code until there is no instruction left. So when 
JPF steps into ThreadInfo.executeStep it will execute int x = 
Verify.getInt(1, 2); and then move to  System.out.println("divide");.
The state information will not be used because state comparision is done 
in higher level than ThreadInfo.executeStep.

I hope I was clear and the most important I didn't write untrue information.

Yours sincerely

       Mateusz Ujma

Michal Kebrt pisze:
> Hi,
>
> I have the following JUnit test executed under JPF.
>
> public class MathTest {
> 	@Test
> 	public void add() {
> 		System.out.println("add");
> 		int x = Verify.getInt(1, 2);
> 	}
>
> 	@Test
> 	public void divide() throws Exception {
> 		System.out.println("divide");
> 	}
> }
>
> And I'm curious why the second test 'divide' is run twice. Firstly I thought 
> it's clear, the 'add' test generates two values in the variable 'x' so the 
> division will be invoked twice as well. But later I realized that x is a local 
> variable that shouldn't affect the rest of the class. I think the state of VM 
> before the division is invoked should be the same in both cases. Am I right or not?
>
> Thanks
>
> Michal
>
> ------------------------------------------------------------------------------
> 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-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel
>
>   

Re: [Javapathfinder-devel] State seen

[Michal K. <mic...@gm...>]

Hi,

it sounds good. Thank you!

MK

Mateusz Ujma wrote:
> Hi,
> 
>    I did some debbuging and here what I've got.
>> I think the state of VM before the division is invoked should be the 
>> same in both cases. Am I right or not?
>>   
>    Yes you are right the state is the same. I've checked that by adding 
> some code into NativePeer.executeMethod() which is invoked for example 
> when JPF finds
> "System.out.println("divide");". But after learning that, I get 
> confused, because I thought if the state has been seen already seen, JPF 
> should not execute
> any more code on that path. I did some more debugging and that's why it 
> executes all the code:
>    After printing first "divide" JPF backtracks to "int x = 
> Verify.getInt(1, 2); ". And starts to execute this code, execution of 
> this code is done in ThreadInfo.executeStep method.
> This method executes code until there is no instruction left. So when 
> JPF steps into ThreadInfo.executeStep it will execute int x = 
> Verify.getInt(1, 2); and then move to  System.out.println("divide");.
> The state information will not be used because state comparision is done 
> in higher level than ThreadInfo.executeStep.
> 
> I hope I was clear and the most important I didn't write untrue 
> information.
> 
> Yours sincerely
> 
>       Mateusz Ujma
> 
> Michal Kebrt pisze:
>> Hi,
>>
>> I have the following JUnit test executed under JPF.
>>
>> public class MathTest {
>>     @Test
>>     public void add() {
>>         System.out.println("add");
>>         int x = Verify.getInt(1, 2);
>>     }
>>
>>     @Test
>>     public void divide() throws Exception {
>>         System.out.println("divide");
>>     }
>> }
>>
>> And I'm curious why the second test 'divide' is run twice. Firstly I 
>> thought it's clear, the 'add' test generates two values in the 
>> variable 'x' so the division will be invoked twice as well. But later 
>> I realized that x is a local variable that shouldn't affect the rest 
>> of the class. I think the state of VM before the division is invoked 
>> should be the same in both cases. Am I right or not?
>>
>> Thanks
>>
>> Michal
>>
>> ------------------------------------------------------------------------------ 
>>
>> 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-devel mailing list
>> Jav...@li...
>> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel
>>
>>   
>