From 24a0385288ecaa3a5027a28d0484e5fe2fee2301 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 27 Mar 2020 16:49:04 -0700 Subject: [PATCH] Fixing a bug: off-by-one error in the executed trace checking. --- src/main/gov/nasa/jpf/listener/StateReducer.java | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index 91c0b11..94b78f8 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -602,9 +602,7 @@ public class StateReducer extends ListenerAdapter { // When we see a choice list shorter than the upper bound, e.g., [3,2] for choices 0,1,2, and 3, // then we have to pad the beginning before we store it, because [3,2] actually means [0,1,3,2] - // First, calculate the difference between this choice list and the upper bound - // The actual list doesn't include '-1' at the end - int actualListLength = newChoiceList.length - 1; + int actualListLength = newChoiceList.length; int diff = maxUpperBound - actualListLength; StringBuilder sb = new StringBuilder(); // Pad the beginning if necessary @@ -613,7 +611,7 @@ public class StateReducer extends ListenerAdapter { } // Then continue with the actual choice list // We don't include the '-1' at the end - for (int i = 0; i < newChoiceList.length - 1; i++) { + for (int i = 0; i < newChoiceList.length; i++) { sb.append(newChoiceList[i]); } return sb.toString(); -- 2.34.1