Differences

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

--- jpf-native:start [2009/05/14 20:45] – franck
+++ jpf-native:start [2009/05/14 21:03] (current) – franck
@@ Line 109: / Line 109: @@
 ===== Model Class =====
+We can model the toString method of the Date class as follows.
+<code java>
+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";
+    }
+}
+</code>
+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.
+<code>
+vm.bootclasspath+= ,modeldirectory
+</code>
+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.
+<code>
+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
+</code>
+===== Model Class and Native Peer Class =====
+We can also "model" the toString method by declaring it native.
+<code java>
+package java.util;
+/**
+ * Model class of the constructor and the toString method of the Date class.
+ */
+public class Date
+{
+    private long fastTime;
+    public Date()
+    {
+        this.fastTime = System.currentTimeMillis();
+    }
+    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>