Consider, for example, the following app.

import java.util.Date;
 
public class Now
{
    public static void main(String[] args)
    {
        Date now = new Date();
        System.out.println(now);
    }
}

If we run JPF on this app, we get something like

JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
 
 
====================================================== system under test
application: Now.java
 
====================================================== search started: 5/14/09 4:43 PM
 
====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: sun.misc.VM.initialize()V (no peer)
        at sun.misc.VM.<clinit>(VM.java:332)
        at java.nio.charset.Charset.atBugLevel(Charset.java:250)
        at java.nio.charset.Charset.checkName(Charset.java:272)
        at java.nio.charset.Charset.<init>(Charset.java:611)
        at sun.nio.cs.Unicode.<init>(Unicode.java:16)
        at sun.nio.cs.UTF_8.<init>(UTF_8.java:39)
        at sun.nio.cs.FastCharsetProvider.lookup(FastCharsetProvider.java:105)
        at sun.nio.cs.FastCharsetProvider.charsetForName(FastCharsetProvider.java:119)
        at java.nio.charset.Charset.lookup2(Charset.java:450)
        at java.nio.charset.Charset.lookup(Charset.java:438)
        at java.nio.charset.Charset.isSupported(Charset.java:480)
        at java.lang.StringCoding.lookupCharset(StringCoding.java:85)
        at java.lang.StringCoding.decode(StringCoding.java:165)
        at java.lang.String.<init>(String.java:444)
        at sun.util.calendar.ZoneInfoFile.getZoneAliases(ZoneInfoFile.java:777)
        at sun.util.calendar.ZoneInfo.getAliasTable(ZoneInfo.java:777)
        at sun.util.calendar.ZoneInfo.getTimeZone(ZoneInfo.java:608)
        at java.util.TimeZone.getTimeZone(TimeZone.java:469)
        at java.util.TimeZone.setDefaultZone(TimeZone.java:566)
        at java.util.TimeZone.getDefaultRef(TimeZone.java:533)
        at java.util.Date.normalize(Date.java:1176)
        at java.util.Date.toString(Date.java:1010)
        at gov.nasa.jpf.ConsoleOutputStream.println(ConsoleOutputStream.java:83)        at Now.main(Now.java:8)
 
 
====================================================== trace #1
------------------------------------------------------ transition #0 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
      [17631 insn w/o sources]
 
====================================================== snapshot #1
thread index=0,name=main,status=RUNNING,this=java.lang.Thread@0,target=null,priority=5,lockCount=0
  owned locks:java.lang.Class@373,java.lang.Class@423,sun.nio.cs.StandardCharsets@1253,java.lang.Class@721
  call stack:
        at sun.misc.VM.<clinit>(VM.java:332)
        at java.nio.charset.Charset.atBugLevel(Charset.java:250)
        at java.nio.charset.Charset.checkName(Charset.java:272)
        at java.nio.charset.Charset.<init>(Charset.java:611)
        at sun.nio.cs.Unicode.<init>(Unicode.java:16)
        at sun.nio.cs.UTF_8.<init>(UTF_8.java:39)
        at sun.nio.cs.FastCharsetProvider.lookup(FastCharsetProvider.java:105)
        at sun.nio.cs.FastCharsetProvider.charsetForName(FastCharsetProvider.java:119)
        at java.nio.charset.Charset.lookup2(Charset.java:450)
        at java.nio.charset.Charset.lookup(Charset.java:438)
        at java.nio.charset.Charset.isSupported(Charset.java:480)
        at java.lang.StringCoding.lookupCharset(StringCoding.java:85)
        at java.lang.StringCoding.decode(StringCoding.java:165)
        at java.lang.String.<init>(String.java:444)
        at sun.util.calendar.ZoneInfoFile.getZoneAliases(ZoneInfoFile.java:777)
        at sun.util.calendar.ZoneInfo.getAliasTable(ZoneInfo.java:777)
        at sun.util.calendar.ZoneInfo.getTimeZone(ZoneInfo.java:608)
        at java.util.TimeZone.getTimeZone(TimeZone.java:469)
        at java.util.TimeZone.setDefaultZone(TimeZone.java:566)
        at java.util.TimeZone.getDefaultRef(TimeZone.java:533)
        at java.util.Date.normalize(Date.java:1176)
        at java.util.Date.toString(Date.java:1010)
        at gov.nasa.jpf.ConsoleOutputStream.println(ConsoleOutputStream.java:83)        at Now.main(Now.java:8)
 
 
====================================================== results
error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: sun.misc.VM.initia..."
 
====================================================== statistics
elapsed time:       0:00:02
states:             new=0, visited=1, backtracked=0, end=0
search:             maxDepth=0, constraints=0
choice generators:  thread=1, data=0
heap:               gc=1, new=1842, free=48
instructions:       17631
max memory:         17MB
loaded code:        classes=137, methods=2029
 
====================================================== search finished: 5/14/09 4:43 PM

During the model checking of the app, JPF encounters some native code.

JPF has two ways to handle native code:

• model class
• native peer class

We can model the toString method of the Date class as follows.

package java.util;
 
/**
 * A model class for the toString method of the Date class.
 */
public class Date
{
    public String toString()
    {
        return "string representation of a Date object in the model class";
    }
}

To ensure that JPF model checks the above class, rather than the Date class of the Java standard library, whenever the toString method is invoked, we add the following to our jpf.properties file.

vm.bootclasspath+= ,modeldirectory

Note that modeldirectory is the directory in which the model classes can be found. This directory contains java/util/Date.java.

If we run JPF, we get something like the following.

JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
                                                                                
                                                                                
====================================================== system under test
application: Now.java
                                                                                
====================================================== search started: 5/14/09 4:52 PM
string representation of a Date object in the model class
                                                                                
====================================================== results
no errors detected
                                                                                
====================================================== statistics
elapsed time:       0:00:01
states:             new=1, visited=0, backtracked=0, end=1
search:             maxDepth=0, constraints=0
choice generators:  thread=1, data=0
heap:               gc=1, new=262, free=12
instructions:       2708
max memory:         10MB
loaded code:        classes=66, methods=839
                                                                                
====================================================== search finished: 5/14/09 4:52 PM

We can also model the

package java.util;
 
/**
 * Model class
 */
public class Date
{
    private long fastTime;
 
    public Date()
    {
        this.fastTime = System.currentTimeMillis();
    }
 
    native public String toString();
}