From: rtrimana <rtrimana@uci.edu>
Date: Fri, 28 Feb 2020 21:36:27 +0000 (-0800)
Subject: Fix for a bug in finding the right integer values in the stack frame: need to find... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=27351fe64ae3dac87e94027cfe83ac67d23f4481;p=jpf-core.git

Fix for a bug in finding the right integer values in the stack frame: need to find a value that's not 0 in the frame (previously we only look at offset 0 or 1 because of adapting the function getValue() from a listener for Java code).
---

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 12eb14f..9d2cd19 100644
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -129,7 +129,7 @@ public class ConflictTracker extends ListenerAdapter {
           if (conflicts(u, u2)) {
             //throw new RuntimeException(createErrorMessage(u, u2));
             conflictFound = true;
-	    errorMessage = createErrorMessage(u, u2);
+	        errorMessage = createErrorMessage(u, u2);
           }
         }
       }
@@ -429,7 +429,7 @@ public class ConflictTracker extends ListenerAdapter {
     out.println("----------------------------------- search finished");
 
     //Comment out the following line to print the explored graph
-    // printGraph();
+    printGraph();
   }
 
   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
@@ -446,7 +446,17 @@ public class ConflictTracker extends ListenerAdapter {
 
       lo = frame.peek();
       hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
-	
+
+      // TODO: Fix for integer values (need to dig deeper into the stack frame to find the right value other than 0)
+      // TODO: Seems to be a problem since this is Groovy (not Java)
+      if (type == Types.T_INT || type == Types.T_LONG || type == Types.T_SHORT) {
+        int offset = 0;
+        while (lo == 0) {
+          lo = frame.peek(offset);
+          offset++;
+        }
+      }
+
       return(decodeValue(type, lo, hi));
     }