Differences

This shows you the differences between two versions of the page.

--- jpf-native:start [2009/05/14 20:56] – franck
+++ jpf-native:start [2009/05/14 21:03] (current) – franck
@@ Line 161: / Line 161: @@
 ===== Model Class and Native Peer Class =====
-We can also model the
+We can also "model" the toString method by declaring it native.
 <code java>
 package java.util;
 /**
- * Model class
+ * Model class of the constructor and the toString method of the Date class.
  */
 public class Date
@@ Line 180: / Line 179: @@
     native public String toString();
 }
+</code>
+Note that we also model the constructor.  This is done since JPF uses the attribute fastTime internally.
+Whenever JPF encounters a native method, it looks for a corresponding
+native peer class.  In this case, we can use the following class.
+<code java>
+package gov.nasa.jpf.jvm;
+/**
+ * Native peer for the toString method of the Date class.
+ */
+public class JPF_java_util_Date
+{
+    public static int toString(MJIEnv env, int objref)
+    {
+        return env.newString(env.getDateObject(objref).toString());
+    }
+}
+</code>
+We have to ensure that the native peer class is part of the classpath
+used by JPF and set the vm.bootclasspath appropriately for the model class.
+If we run JPF, we get something like the following.
+<code>
+JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
+====================================================== system under test
+application: Now.java
+====================================================== search started: 5/14/09 5:02 PM
+Thu May 14 17:02:54 EDT 2009
+====================================================== 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=14
+instructions:       2709
+max memory:         17MB
+loaded code:        classes=66, methods=839
+====================================================== search finished: 5/14/09 5:02 PM
 </code>