From: rtrimana <rtrimana@uci.edu>
Date: Tue, 7 Jul 2020 22:40:53 +0000 (-0700)
Subject: Adding notes in the latest changes for the serializer bug fix.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=cb0dd97fb75d3ef79006b4e2914e630847cb9338;ds=sidebyside

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 c34e1c1..9ed932b 100644
--- 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
+  // 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;
 
 
diff --git a/src/main/gov/nasa/jpf/vm/JPFOutputStream.java b/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
index 9b4fbbe..5b32693 100644
--- 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();
-    
+
+    // 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);
     
diff --git a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
index 0f6eb0e..efaf25a 100644
--- 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
+  // 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;
 
diff --git a/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
index 589f53e..9cdb54b 100644
--- 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();
+    // 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;