JPF has two ways to handle native code:

• model class
• native peer class

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);
    }
}