Adding notes in the latest changes for the serializer bug fix.

diff --git a/src/main/gov/nasa/jpf/vm/ElementInfo.java b/src/main/gov/nasa/jpf/vm/ElementInfo.java
index c34e1c104977ea82eb09c0f474bc0e0a60856992..9ed932bc33ebbf4f97c6b534d3ae101d42d212f4 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/ElementInfo.java
+++ b/src/main/gov/nasa/jpf/vm/ElementInfo.java
@@ -137,6 +137,8 @@ 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
 
   // cache for a serialized representation of the object, which can be used
   // by state-matching. Value interpretation depends on the configured Serializer

+  // TODO: Fix for Groovy's model-checking
+  // TODO: Change of sid assignment strategy since the previous one caused a bug with SmartThings object filtering

   protected long sid;
 
 
   protected long sid;
 
 

diff --git a/src/main/gov/nasa/jpf/vm/JPFOutputStream.java b/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
index 9b4fbbe15f72fdc6d78ab4d3b9ffbaedc76b75d5..5b32693fc6d8be3ef89d1119463bea764c444535 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
+++ b/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
@@ -120,7 +120,9 @@ public class JPFOutputStream extends OutputStream {
   public void print (ElementInfo ei, FinalBitSet filterMask){
     boolean isObject = ei.isObject();
     ClassInfo ci = ei.getClassInfo();
   public void print (ElementInfo ei, FinalBitSet filterMask){
     boolean isObject = ei.isObject();
     ClassInfo ci = ei.getClassInfo();

-    
+
+    // TODO: Fix for Groovy's model-checking
+    // TODO: Change of sid assignment strategy since the previous one caused a bug with SmartThings object filtering

     int ref = (useSid) ? ((int)ei.getSid()) : ei.getObjectRef();
     ps.printf("@%x ", ref);
     
     int ref = (useSid) ? ((int)ei.getSid()) : ei.getObjectRef();
     ps.printf("@%x ", ref);
     

diff --git a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
index 0f6eb0e0e77eee12a1e9551cb4f9f6ff32de3104..efaf25ae90c578d78fa47548799d81c8f54e1b4d 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
@@ -55,6 +55,8 @@ 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
   // 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

+  // TODO: Fix for Groovy's model-checking
+  // TODO: Change of sid assignment strategy since the previous one caused a bug with SmartThings object filtering

   long initsidCount=0;
   long sidCount=1;
 
   long initsidCount=0;
   long sidCount=1;
 

diff --git a/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
index 589f53eee0f1bba68fc0fcf6cfc4a8db033c08a5..9cdb54b4bf57c81b6f14337d35e94befb7ddb324 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
@@ -156,6 +156,8 @@ public class SmartThingsConfig
   @Override
   public FramePolicy ammendFramePolicy(MethodInfo mi, FramePolicy sofar) {
     ClassInfo ci = mi.getClassInfo();
   @Override
   public FramePolicy ammendFramePolicy(MethodInfo mi, FramePolicy sofar) {
     ClassInfo ci = mi.getClassInfo();

+    // TODO: Fix for Groovy's model-checking
+    // TODO: Change of sid assignment strategy since the previous one caused a bug with SmartThings object filtering

     if (ignoreClass(ci) || checkName(mi.getName())) {
       sofar.includeLocals = false;
       sofar.includeOps = false;
     if (ignoreClass(ci) || checkName(mi.getName())) {
       sofar.includeLocals = false;
       sofar.includeOps = false;