javapathfinder-devel

[Javapathfinder-devel] JUnit exceptions

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

Hello,

I've just tried to run the Racer example under JPF+JUnit. It correctly prints 
'10' twice and then 'java.lang.ArithmeticException: division by zero'. But this 
exception is eaten in JUnit internals so the propertyViolated method is not 
called. Is there a way to get execution history (as shown in example) in such 
situation? Throwing exception out of JUnit would probably help but I would to 
avoid it. I don't want to modify neither JUnit nor JPF, just want to extend both 
of them.

Michal

Re: [Javapathfinder-devel] JUnit exceptions

[Peter C. M. <Pet...@na...>]

this is the problem I was thinking of - if you run JUnit under JPF,  
the JUnit exception firewall is a perfectly fine exception handler  
from JPF's perspective, so NoUnhandledExceptionProperty is never  
violated. You can't say JUnit is part of the SuT, but a little less  
than the rest. Both vm.halt_on_throw and overriding  
JVM.handleException() are hacks in this case. The only clean solution  
I see is to create a new PropertyListener, say JUnitProperty, which  
monitors exceptionThrown, and turns the ones underneath JUnit into  
property violations

-- Peter




On Sep 24, 2008, at 11:31 AM, Michal Kebrt wrote:

> Hello,
>
> I've just tried to run the Racer example under JPF+JUnit. It  
> correctly prints
> '10' twice and then 'java.lang.ArithmeticException: division by  
> zero'. But this
> exception is eaten in JUnit internals so the propertyViolated method  
> is not
> called. Is there a way to get execution history (as shown in  
> example) in such
> situation? Throwing exception out of JUnit would probably help but I  
> would to
> avoid it. I don't want to modify neither JUnit nor JPF, just want to  
> extend both
> of them.
>
> Michal
>
> -------------------------------------------------------------------------
> This SF.Net email is sponsored by the Moblin Your Move Developer's  
> challenge
> Build the coolest Linux based applications with Moblin SDK & win  
> great prizes
> Grand prize is a trip for two to an Open Source event anywhere in  
> the world
> http://moblin-contest.org/redirect.php?banner_id=100&url=/
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel

Re: [Javapathfinder-devel] JUnit exceptions

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

After writing a part of JUnitProperty I realized it wouldn't be so 
straightforward as it seemed to be. For example, JUnit has @Test(expected=...) 
annotation which shouldn't produce an error when expected exception occurs. 
Therefore the JUnitProperty should understand some of JUnit internals which is 
not very clean solution.

I am thinking of inspecting JVM Path object (and maybe other information 
provided by Reporter) in JUnit's native peer but the path is always empty, why?

MK

Peter C. Mehlitz wrote:
> this is the problem I was thinking of - if you run JUnit under JPF,  
> the JUnit exception firewall is a perfectly fine exception handler  
> from JPF's perspective, so NoUnhandledExceptionProperty is never  
> violated. You can't say JUnit is part of the SuT, but a little less  
> than the rest. Both vm.halt_on_throw and overriding  
> JVM.handleException() are hacks in this case. The only clean solution  
> I see is to create a new PropertyListener, say JUnitProperty, which  
> monitors exceptionThrown, and turns the ones underneath JUnit into  
> property violations
> 
> -- Peter

Re: [Javapathfinder-devel] JUnit exceptions

[Peter C. M. <Pet...@na...>]

If you inspect the path at the end of a JPF run, it is only non-empty  
in case there was a property violation (backtracking to the first  
state and not having any non-processed choice anymore *is* the end  
condition for the search)

-- Peter


On Sep 29, 2008, at 6:13 AM, Michal Kebrt wrote:

> After writing a part of JUnitProperty I realized it wouldn't be so  
> straightforward as it seemed to be. For example, JUnit has  
> @Test(expected=...) annotation which shouldn't produce an error when  
> expected exception occurs. Therefore the JUnitProperty should  
> understand some of JUnit internals which is not very clean solution.
>
> I am thinking of inspecting JVM Path object (and maybe other  
> information provided by Reporter) in JUnit's native peer but the  
> path is always empty, why?
>
> MK

Re: [Javapathfinder-devel] JUnit exceptions

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

No it is not at the end of a JPF run. It's in a native peer for JUnit listener, 
e.g.:
public static void testStartedNative(MJIEnv env, int robj, int rString0) {
   System.out.println(env.getJPF().getReporter().getPath().size());
}

MK

Peter C. Mehlitz wrote:
> If you inspect the path at the end of a JPF run, it is only non-empty  
> in case there was a property violation (backtracking to the first  
> state and not having any non-processed choice anymore *is* the end  
> condition for the search)
> 
> -- Peter
> 
> 
> On Sep 29, 2008, at 6:13 AM, Michal Kebrt wrote:
> 
>> After writing a part of JUnitProperty I realized it wouldn't be so  
>> straightforward as it seemed to be. For example, JUnit has  
>> @Test(expected=...) annotation which shouldn't produce an error when  
>> expected exception occurs. Therefore the JUnitProperty should  
>> understand some of JUnit internals which is not very clean solution.
>>
>> I am thinking of inspecting JVM Path object (and maybe other  
>> information provided by Reporter) in JUnit's native peer but the  
>> path is always empty, why?
>>
>> MK
> 
> 
> -------------------------------------------------------------------------
> This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
> Build the coolest Linux based applications with Moblin SDK & win great prizes
> Grand prize is a trip for two to an Open Source event anywhere in the world
> http://moblin-contest.org/redirect.php?banner_id=100&url=/
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel