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
>
>