Integrating bug fix for CFSerializer.

diff --git a/src/main/gov/nasa/jpf/vm/ElementInfo.java b/src/main/gov/nasa/jpf/vm/ElementInfo.java
index d853afb37a88585f77a4bfdf2ff43575562f70f7..c34e1c104977ea82eb09c0f474bc0e0a60856992 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/ElementInfo.java
+++ b/src/main/gov/nasa/jpf/vm/ElementInfo.java
@@ -137,7 +137,7 @@ public abstract class ElementInfo implements Cloneable {
 
   // cache for a serialized representation of the object, which can be used
   // by state-matching. Value interpretation depends on the configured Serializer
-  protected int sid;
+  protected long sid;
 
 
   // helpers for state storage/restore processing, to avoid explicit iterators on
@@ -259,11 +259,11 @@ public abstract class ElementInfo implements Cloneable {
   
   
   //--- sids are only supposed to be used by the Serializer
-  public void setSid(int id){
+  public void setSid(long id){
     sid = id;
   }
 
-  public int getSid() {
+  public long getSid() {
     return sid;
   }
 

diff --git a/src/main/gov/nasa/jpf/vm/JPFOutputStream.java b/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
index 71dfb9f7c076ea621de9e230bab1d79d1f8550c7..9b4fbbe15f72fdc6d78ab4d3b9ffbaedc76b75d5 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
+++ b/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
@@ -121,7 +121,7 @@ public class JPFOutputStream extends OutputStream {
     boolean isObject = ei.isObject();
     ClassInfo ci = ei.getClassInfo();
     
-    int ref = (useSid) ? ei.getSid() : ei.getObjectRef();
+    int ref = (useSid) ? ((int)ei.getSid()) : ei.getObjectRef();
     ps.printf("@%x ", ref);
     
     if (isObject){

diff --git a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
index f6663eb31b94338b54e8a09e9eafa6ef5091ec1f..0f6eb0e0e77eee12a1e9551cb4f9f6ff32de3104 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
@@ -55,21 +55,14 @@ public class CFSerializer extends FilteringSerializer {
   // over the serialized objects to reset their sids. This works by resetting
   // the sid to 0 upon backtrack, and counting either upwards from 1 or downwards
   // from -1, but store the absolute value in the serialization stream
-  boolean positiveSid;
-
-  int sidCount;
+  long initsidCount=0;
+  long sidCount=1;
 
   @Override
   protected void initReferenceQueue() {
     super.initReferenceQueue();
-
-    if (positiveSid){
-      positiveSid = false;
-      sidCount = -1;
-    } else {
-      positiveSid = true;
-      sidCount = 1;
-    }
+    
+    initsidCount = sidCount - 1;
   }
 
   // might be overriden in subclasses to conditionally queue objects
@@ -86,30 +79,20 @@ public class CFSerializer extends FilteringSerializer {
       ClassInfo ci = ei.getClassInfo();
 
       if (SmartThingsConfig.instance.ignoreClass(ci)) {
-        ei.setSid(0);
+        ei.setSid(initsidCount);
         buf.add(0);
         return;
       }
+      long sid = ei.getSid();
       
-      int sid = ei.getSid();
-
-      if (positiveSid){ // count sid upwards from 1
-        if (sid <= 0){  // not seen before in this serialization run
+      if (sid <= initsidCount){ // count sid upwards from 1
           sid = sidCount++;
           ei.setSid(sid);
           queueReference(ei);
-        }
-      } else { // count sid downwards from -1
-        if (sid >= 0){ // not seen before in this serialization run
-          sid = sidCount--;
-          ei.setSid(sid);
-          queueReference(ei);
-        }
-        sid = -sid;
       }
 
       // note that we always add the absolute sid value
-      buf.add(sid);
+      buf.add((int)(sid - initsidCount));
     }
   }
 
@@ -188,6 +171,6 @@ public class CFSerializer extends FilteringSerializer {
   
   @Override
   protected int getSerializedReferenceValue (ElementInfo ei){
-    return Math.abs(ei.getSid());
+    return (int)(ei.getSid()-initsidCount);
   }
 }