projects
/
jpf-core.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
b562358
)
Fixing a potential bug: if statement that contains updateBacktrackSetsFromGraph was...
author
rtrimana
<rtrimana@uci.edu>
Fri, 11 Dec 2020 00:01:36 +0000
(16:01 -0800)
committer
rtrimana
<rtrimana@uci.edu>
Mon, 14 Dec 2020 19:27:43 +0000
(11:27 -0800)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
patch
|
blob
|
history
diff --git
a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index a0abd98c66033b353d880917c36cce2ab59b6a61..82f3db8bd94a50b0aa290d00f1a50458cf15fd36 100755
(executable)
--- a/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@
-752,8
+752,8
@@
public class DPORStateReducer extends ListenerAdapter {
// Often a transition (choice/event) can result into forwarding/backtracking to a number of states
boolean terminate = false;
for(Integer stateId : justVisitedStates) {
// Often a transition (choice/event) can result into forwarding/backtracking to a number of states
boolean terminate = false;
for(Integer stateId : justVisitedStates) {
- // We
only flip the value of terminate once ...
- if (
!terminate &&
prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
+ // We
perform updates on backtrack sets for every
+ if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
updateBacktrackSetsFromGraph(stateId);
terminate = true;
}
updateBacktrackSetsFromGraph(stateId);
terminate = true;
}