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