From e74d8836549c19fbd0133fee203de08a6328d370 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 14:32:02 +0200
Subject: [PATCH] Fix NPE in OutputCollector.addStateToTrace
This is a breaking change - callers now need to check for isEmpty()
instead of null.
---
.../src/tlc2/output/OutputCollector.java | 5 +----
1 file changed, 1 insertion(+), 4 deletions(-)
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/output/OutputCollector.java b/tlatools/org.lamport.tlatools/src/tlc2/output/OutputCollector.java
index 55a832033..b70394345 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/output/OutputCollector.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/output/OutputCollector.java
@@ -17,7 +17,7 @@ import tlc2.tool.TLCStateInfo;
public class OutputCollector {
private static TLCState initialState = null;
- private static List<TLCStateInfo> trace = null;
+ private static List<TLCStateInfo> trace = new ArrayList<>();
private static List<Message> allMessages = new ArrayList<>();
private static Map<Location, Long> lineCount = new HashMap<>();
private static ModuleNode moduleNode = null;
@@ -32,9 +32,6 @@ public class OutputCollector {
}
public static void addStateToTrace(TLCStateInfo tlcStateInfo) {
- if (trace == null) {
- trace = new ArrayList<>();
- }
trace.add(tlcStateInfo);
}
--
GitLab