From 38b127930aa7036b8367d9bb9a5daa520215bfbf Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Thu, 16 Apr 2020 20:48:14 -0700
Subject: [PATCH] TLC reports bogus "Wrong invocation of TLC error printer.
Error code not found." for some runtime errors.
[Bug][TLC]
---
tlatools/org.lamport.tlatools/src/util/Assert.java | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/tlatools/org.lamport.tlatools/src/util/Assert.java b/tlatools/org.lamport.tlatools/src/util/Assert.java
index 3cb19484e..99a054407 100644
--- a/tlatools/org.lamport.tlatools/src/util/Assert.java
+++ b/tlatools/org.lamport.tlatools/src/util/Assert.java
@@ -4,6 +4,7 @@
package util;
+import tlc2.output.EC;
import tlc2.output.MP;
/**
@@ -101,7 +102,7 @@ public class Assert
{
if (!condition)
{
- throw new TLCRuntimeException(MP.getMessage(errorCode));
+ throw new TLCRuntimeException(errorCode, MP.getMessage(errorCode));
}
}
@@ -135,7 +136,7 @@ public class Assert
public TLCRuntimeException(String errorMsg) {
super(errorMsg);
- this.errorCode = -1; // Unknown error code.
+ this.errorCode = EC.GENERAL; // Unknown error code.
}
public TLCRuntimeException(int errorCode, String message) {
--
GitLab