Logging and JPF

[Chris Powell]

Using the standard Logger doesn't work in JPF as:

:
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native sun.reflect.Reflection.getCallerClass
    at sun.reflect.Reflection.getCallerClass(gov.nasa.jpf.jvm.JPF_sun_reflect_Reflection)
    at java.util.logging.Logger.getLogger(java/util/logging/Logger.java:2)
:

(and sun.reflect.Reflection is in rt.jar).

So I tried to use the JPF logger (btw, the example code on the JPF site won't work because of the missing gov.nasa.jpf.JPF import):

import java.util.logging.Level;
import java.util.logging.Logger;

import gov.nasa.jpf.JPF;

public class Test2
{
    static final Logger logger = JPF.getLogger("Test2");

    public static void main(String[]S)
    {
        logger.setLevel(Level.FINER);
        logger.info( "  ...MAIN" );
    }
}

which runs fine on its own.  Running using JPF I get:

[FINER] registering class: sun.misc.SharedSecrets
[FINER] resolve classinfo: sun.misc.Unsafe
[FINER] resolving superclass: java.lang.Object of sun.misc.Unsafe
[FINER] registering class: sun.misc.Unsafe
[FINER] resolve classinfo: gov.nasa.jpf.JPF
[SEVERE] JPF exception, terminating: gov.nasa.jpf.JPF
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.jvm.NoClassInfoException: gov.nasa.jpf.JPF
    at gov.nasa.jpf.jvm.ClassInfo.loadClass(ClassInfo.java:1214)
    at gov.nasa.jpf.jvm.ClassInfo.getResolvedClassInfo(ClassInfo.java:1207)
    at gov.nasa.jpf.jvm.bytecode.INVOKESTATIC.getClassInfo(INVOKESTATIC.java:46)
    at gov.nasa.jpf.jvm.bytecode.INVOKESTATIC.execute(INVOKESTATIC.java:86)
    at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:2245)
    at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:2197)
    at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:781)
    at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1794)
    at gov.nasa.jpf.search.Search.forward(Search.java:533)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
    at gov.nasa.jpf.JPF.run(JPF.java:618)
    at gov.nasa.jpf.JPF.start(JPF.java:190)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
    at java.lang.reflect.Method.invoke(Unknown Source)
    at gov.nasa.jpf.tool.Run.call(Run.java:76)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:100)

(This 'missing' gov.nasa.jpf.JPF was mentioned in a prior question but not answered).  How then, do I use logging within JPF?