From b49d73a21fbf80e60a3ce095b4e2f49d07bede52 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 14 Feb 2020 10:32:06 -0800 Subject: [PATCH 1/1] Fixing an out of bound bug. --- src/main/gov/nasa/jpf/listener/StateReducer.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index 4740583..93043fa 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -300,8 +300,8 @@ public class StateReducer extends ListenerAdapter { if (stateReductionMode) { // Update vodGraph int currChoice = choiceCounter - 1; - if (currChoice < 0 || choices[currChoice] == -1 || prevChoiceValue == choices[currChoice]) { - // Current choice has to be at least 0 (initial case can be -1) + if (currChoice < 0 || currChoice > choices.length - 1 || choices[currChoice] == -1 || prevChoiceValue == choices[currChoice]) { + // Handle all corner cases (e.g., out of bound values) return; } // When current choice is 0, previous choice could be -1 -- 2.34.1