javapathfinder-user

[Javapathfinder-user] JPF+JUnit

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

Hello,

I'm trying to run my JUnit tests through JPF but I still cannot succeed. The 
test looks like this:

import org.junit.Test;
import static org.junit.Assert.*;

public class Simple {

     public static void main(String[] args) {
         System.out.println("Hello");
         assertEquals( 4, 4 );
     }

     @Test
     public void add() {
         assertEquals( 4, 4 );
     }
}

When I run it using:

./jpf +vm.classpath=/mypath/junit/junit-4.4.jar:/mypath/junit 
org.junit.runner.JUnitCore Simple

the following error occurs:

gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.reflect.InvocationTargetException: in java.lang.Class.getAnnotations : 
java.lang.NullPointerException
         at java.lang.Class.getAnnotations(Native Method)
         at 
org.junit.internal.runners.JUnit4ClassRunner.classAnnotations(JUnit4ClassRunner.java:64)
         at 
org.junit.internal.runners.JUnit4ClassRunner.getDescription(JUnit4ClassRunner.java:56)
         at 
org.junit.internal.runners.CompositeRunner.getDescription(CompositeRunner.java:40)
         at org.junit.runner.JUnitCore.run(JUnitCore.java:129)
         at org.junit.runner.JUnitCore.run(JUnitCore.java:109)
         at org.junit.runner.JUnitCore.run(JUnitCore.java:100)
         at org.junit.runner.JUnitCore.runMain(JUnitCore.java:81)
         at org.junit.runner.JUnitCore.main(JUnitCore.java:44)

When I run the test without JPF, it works fine. When I run JPF with 'Simple' 
program as an input, it also works fine. Is there some way how to run JPF on 
that test without explicitly writing the main method for each test class as you 
do in your JPF Test Tystem?

Is this problem connected with some reflection limitations in JPF as can be 
found here:
http://sourceforge.net/mailarchive/message.php?msg_id=e3a26fee0605222246x6f3f600as1f9d0484047fa3ce%40mail.google.com

Thanks for answer.

Michal Kebrt

Re: [Javapathfinder-user] JPF+JUnit

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

fixed

-- Peter



On Aug 13, 2008, at 6:07 AM, Michal Kebrt wrote:

> Hello,
>
> I'm trying to run my JUnit tests through JPF but I still cannot  
> succeed. The
> test looks like this:
>
> import org.junit.Test;
> import static org.junit.Assert.*;
>
> public class Simple {
>
>     public static void main(String[] args) {
>         System.out.println("Hello");
>         assertEquals( 4, 4 );
>     }
>
>     @Test
>     public void add() {
>         assertEquals( 4, 4 );
>     }
> }
>
> When I run it using:
>
> ./jpf +vm.classpath=/mypath/junit/junit-4.4.jar:/mypath/junit
> org.junit.runner.JUnitCore Simple
>
> the following error occurs:
>
> gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
> java.lang.reflect.InvocationTargetException: in  
> java.lang.Class.getAnnotations :
> java.lang.NullPointerException
>         at java.lang.Class.getAnnotations(Native Method)
>         at
> org 
> .junit 
> .internal 
> .runners.JUnit4ClassRunner.classAnnotations(JUnit4ClassRunner.java:64)
>         at
> org 
> .junit 
> .internal 
> .runners.JUnit4ClassRunner.getDescription(JUnit4ClassRunner.java:56)
>         at
> org 
> .junit 
> .internal 
> .runners.CompositeRunner.getDescription(CompositeRunner.java:40)
>         at org.junit.runner.JUnitCore.run(JUnitCore.java:129)
>         at org.junit.runner.JUnitCore.run(JUnitCore.java:109)
>         at org.junit.runner.JUnitCore.run(JUnitCore.java:100)
>         at org.junit.runner.JUnitCore.runMain(JUnitCore.java:81)
>         at org.junit.runner.JUnitCore.main(JUnitCore.java:44)
>
> When I run the test without JPF, it works fine. When I run JPF with  
> 'Simple'
> program as an input, it also works fine. Is there some way how to  
> run JPF on
> that test without explicitly writing the main method for each test  
> class as you
> do in your JPF Test Tystem?
>
> Is this problem connected with some reflection limitations in JPF as  
> can be
> found here:
> http://sourceforge.net/mailarchive/message.php?msg_id=e3a26fee0605222246x6f3f600as1f9d0484047fa3ce%40mail.google.com
>
> Thanks for answer.
>
> Michal Kebrt
>
> -------------------------------------------------------------------------
> 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-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user

[Javapathfinder-user] JPF+RMI

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

Hello,

thanks for Peter's fix. I'm experimenting with JPF launched together with JUnit. 
The purpose of my work is to run JPF on a JUnit test. I would like to use 
JUnit's RunListener and also JPF's listeners to be informed what's currenly 
being done. I've successfully tested JPF's SearchListener. Now I'm testing 
JUnit's listener and looking for a way of how to receive information from that 
listener in an external program (for example in the program which invokes JPF.run).

My first idea was to use RMI - after the JUnit listener is called it calls RMI 
server. Without JPF it works perfectly. Unfortunately when I run JPF on JUnit 
with such listener it ends with the following error:

java.lang.UnsatisfiedLinkError: java.net.InetAddress.init()V (no peer)
         at java.net.InetAddress.<clinit>(InetAddress.java:216)
         at sun.rmi.transport.tcp.TCPEndpoint.<clinit>(TCPEndpoint.java:95)
         at java.rmi.registry.LocateRegistry.getRegistry(LocateRegistry.java:158)
         at java.rmi.registry.LocateRegistry.getRegistry(LocateRegistry.java:106)
         at java.rmi.Naming.getRegistry(Naming.java:204)
         at java.rmi.Naming.lookup(Naming.java:80)
         at cz.kebrt.jpf.JUnitListener.<init>(JUnitListener.java:22)
         at org.junit.runner.JUnitCore.runMainAndExit(JUnitCore.java:57)
         at org.junit.runner.JUnitCore.main(JUnitCore.java:48)

I'm not sure whether all information on JPF web are uptodate but there's 
information about missing support for java.net. If it's true that would be the 
cause of my problem.

What kind of IPC between JUnit listener and other program would you recommend? 
Files?

Thanks.

Michal Kebrt

Re: [Javapathfinder-user] JPF+RMI

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

Hi Michal,

yes and no. Yes - we don't model java.net yet (although that is in the  
works as part of Google's Summer of Code). And no - it's probably not  
what you want anyways if your RunListener is supposed to monitor test  
execution outside of JPF. You have to be aware of that you execute  
JUnit under JPF, which means you might backtrack. If an outside  
listener would make any sense, you could use MJI to notify it, but it  
would have to be aware of backtracking

Please make sure you don't want it the other way round, executing JPF  
under JUnit (like the JPF regression tests do, there's also some  
documentation for the associated infrastructure like TestJPF etc.).  
This is the far more common case.

-- Peter

On Aug 16, 2008, at 8:51 AM, Michal Kebrt wrote:

> Hello,
>
> thanks for Peter's fix. I'm experimenting with JPF launched together  
> with JUnit.
> The purpose of my work is to run JPF on a JUnit test. I would like  
> to use
> JUnit's RunListener and also JPF's listeners to be informed what's  
> currenly
> being done. I've successfully tested JPF's SearchListener. Now I'm  
> testing
> JUnit's listener and looking for a way of how to receive information  
> from that
> listener in an external program (for example in the program which  
> invokes JPF.run).
>
> My first idea was to use RMI - after the JUnit listener is called it  
> calls RMI
> server. Without JPF it works perfectly. Unfortunately when I run JPF  
> on JUnit
> with such listener it ends with the following error:
>
> java.lang.UnsatisfiedLinkError: java.net.InetAddress.init()V (no peer)
>         at java.net.InetAddress.<clinit>(InetAddress.java:216)
>         at  
> sun.rmi.transport.tcp.TCPEndpoint.<clinit>(TCPEndpoint.java:95)
>         at  
> java.rmi.registry.LocateRegistry.getRegistry(LocateRegistry.java:158)
>         at  
> java.rmi.registry.LocateRegistry.getRegistry(LocateRegistry.java:106)
>         at java.rmi.Naming.getRegistry(Naming.java:204)
>         at java.rmi.Naming.lookup(Naming.java:80)
>         at cz.kebrt.jpf.JUnitListener.<init>(JUnitListener.java:22)
>         at org.junit.runner.JUnitCore.runMainAndExit(JUnitCore.java: 
> 57)
>         at org.junit.runner.JUnitCore.main(JUnitCore.java:48)
>
> I'm not sure whether all information on JPF web are uptodate but  
> there's
> information about missing support for java.net. If it's true that  
> would be the
> cause of my problem.
>
> What kind of IPC between JUnit listener and other program would you  
> recommend?
> Files?
>
> Thanks.
>
> Michal Kebrt
>
> -------------------------------------------------------------------------
> 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-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user

Re: [Javapathfinder-user] JPF+RMI

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

Hi Peter,

I'm not sure whether we are talking about same tests and test methods.
Suppose we have the following test (case) with two test methods:

public class MyTestCase {
  @Test
  public void addition() {
    assertEquals(12, simpleMath.add(7, 5));
  }

  @Test
  public void subtraction() {
    assertEquals(9, simpleMath.substract(12, 3));
  }
}

When JUnit runs MyTestCase it runs both methods and reports whether
they finished successfully or not. When the first method fails JUnit
will continue to run the second one. What happens when JUnit is run
under JPF? By default JUnit prints test results on stdout which is not
very useful if I want to collect these results. It is possible to run
JUnit with a different listener that will throw exceptions instead of
printing them on stdout. Such an exception will come to JPF's
propertyViolated - that's ok, but now execution stops and no other
test methods will be run (because JUnit exited with an exception on
some of the previous test method. How to tackle it?

One idea was to add an option into JUnit that would allow to run only
a single test method, which has a disadvantage that @BeforeClass and
@AfterClass initialization methods must be run for each test method.

Do you have any other idea how to be able to run all test methods
under JUnit+JPF so that results can be collected just by a JPF
listener as you suggested earlier.

> The test method itself you can get either from
> Config.getTargetArgParameters(), JVM.getArgs(), or by checking for
> Method.invoke() calls from instructionExecuted() notifications. If you want
> details about failed tests, those you would get from propertyViolated().

Don't you mean test case? In Javadoc there's written
Config.getTargetArgParameters() returns command line arguments passed
to the program executed under JPF. Is it right? In case of JUnit it
means names of test cases (classes) that are to be run (not test
methods).

Thanks.

Michal

On Wed, Aug 27, 2008 at 6:37 PM, Peter C. Mehlitz
<Pet...@na...> wrote:
>>
> Hi Michal,
>
>> Of course, I would rather use an easier solution but I'm not sure
>> whether it could
>> be achieved just by JPF listener. When I execute JUnit under JPF how can I
>> be
>> notified when a single test method has finished? And when an error occurs
>> in one test throwing an exception the whole JPF execution will be stopped
>> after
>> propertyViolated() is called. Is it right? But I would to like to run
>> all test methods
>> regardless they finish with an error or success.
>
> that's simple. You can use the same listener instance for multiple JPF runs
> (== each JUnit test), so you can collect statistics about failed and
> succeeded tests in this listener (which is allocated by your JPF driver).
> The test method itself you can get either from
> Config.getTargetArgParameters(), JVM.getArgs(), or by checking for
> Method.invoke() calls from instructionExecuted() notifications. If you want
> details about failed tests, those you would get from propertyViolated().
>
> -- Peter
>