From ad4ce6133bfbaa53d3b80f6d92a7d947b8a30c80 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Wed, 4 Mar 2020 15:04:58 -0800
Subject: [PATCH] Do not warn on an unmatched operators if Java overrides
disabled warnings.
[Refactor][TLC]
---
tlatools/src/tlc2/overrides/Evaluation.java | 8 ++++++++
.../src/tlc2/overrides/TLAPlusOperator.java | 5 +++++
tlatools/src/tlc2/tool/impl/SpecProcessor.java | 17 ++++++++---------
3 files changed, 21 insertions(+), 9 deletions(-)
diff --git a/tlatools/src/tlc2/overrides/Evaluation.java b/tlatools/src/tlc2/overrides/Evaluation.java
index 9710713bc..2422f4968 100644
--- a/tlatools/src/tlc2/overrides/Evaluation.java
+++ b/tlatools/src/tlc2/overrides/Evaluation.java
@@ -61,4 +61,12 @@ public @interface Evaluation {
* @see tlc2.tool.impl.SpecProcessor.processConstantDefns()
*/
int minLevel() default 0;
+
+ /**
+ * @return true if a warning should be printed when a EV cannot be mapped to the
+ * given TLA+ definition in module.
+ * @see Evaluation#definition()
+ * @see Evaluation#module()
+ */
+ boolean warn() default true;
}
diff --git a/tlatools/src/tlc2/overrides/TLAPlusOperator.java b/tlatools/src/tlc2/overrides/TLAPlusOperator.java
index d00cb0962..780c0f8df 100644
--- a/tlatools/src/tlc2/overrides/TLAPlusOperator.java
+++ b/tlatools/src/tlc2/overrides/TLAPlusOperator.java
@@ -52,4 +52,9 @@ public @interface TLAPlusOperator {
* @see tlc2.overrides.Evaluation.minLevel()
*/
int minLevel() default 0;
+
+ /**
+ * @return tlc2.overrides.Evaluation.warn()
+ */
+ boolean warn() default true;
}
diff --git a/tlatools/src/tlc2/tool/impl/SpecProcessor.java b/tlatools/src/tlc2/tool/impl/SpecProcessor.java
index 58a3b2cd0..71955b61d 100644
--- a/tlatools/src/tlc2/tool/impl/SpecProcessor.java
+++ b/tlatools/src/tlc2/tool/impl/SpecProcessor.java
@@ -589,15 +589,14 @@ public class SpecProcessor implements ValueConstants, ToolGlobals {
final ModuleNode moduleNode = modSet.get(evaluation.module());
if (moduleNode == null) {
- // If the module, for which the operator has been defined, isn't part of the spec,
- // it is probably intentional and thus confusing to warn the user. This e.g.
- // happen with CommunitModules which has a bunch of operators spread over a set
- // modules and a user only uses a subset in her spec.
+ if (evaluation.warn()) MP.printMessage(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_MODULE_MISMATCH,
+ evaluation.module() + "!" + evaluation.definition(),
+ c.getResource(c.getSimpleName() + ".class").toExternalForm(), val.toString());
continue LOOP;
}
final OpDefNode opDef = moduleNode.getOpDef(evaluation.definition());
if (opDef == null) {
- MP.printMessage(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_IDENTIFIER_MISMATCH,
+ if (evaluation.warn()) MP.printMessage(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_IDENTIFIER_MISMATCH,
evaluation.module() + "!" + evaluation.definition(),
c.getResource(c.getSimpleName() + ".class").toExternalForm(), val.toString());
continue LOOP;
@@ -619,24 +618,24 @@ public class SpecProcessor implements ValueConstants, ToolGlobals {
if (opOverrideCandidate != null) {
final ModuleNode moduleNode = modSet.get(opOverrideCandidate.module());
if (moduleNode == null) {
- MP.printWarning(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_MODULE_MISMATCH,
+ if (opOverrideCandidate.warn()) MP.printWarning(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_MODULE_MISMATCH,
opOverrideCandidate.identifier(), opOverrideCandidate.module(), m.toString());
continue LOOP;
}
final OpDefNode opDef = moduleNode.getOpDef(opOverrideCandidate.identifier());
if (opDef == null) {
- MP.printWarning(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_IDENTIFIER_MISMATCH,
+ if (opOverrideCandidate.warn()) MP.printWarning(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_IDENTIFIER_MISMATCH,
opOverrideCandidate.identifier(), opOverrideCandidate.module(), m.toString());
continue LOOP;
}
final Value val = MethodValue.get(m, opOverrideCandidate.minLevel());
if (opDef.getArity() != m.getParameterCount()) {
- MP.printWarning(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_MISMATCH,
+ if (opOverrideCandidate.warn()) MP.printWarning(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_MISMATCH,
opDef.getName().toString(), c.getName(), val.toString());
continue LOOP;
} else {
- MP.printMessage(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_LOADED,
+ if (opOverrideCandidate.warn()) MP.printMessage(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_LOADED,
opDef.getName().toString(), c.getName(),
val instanceof MethodValue ? val.toString() : val.getClass().getName()); // toString of non-MethodValue instances can be expensive.
}
--
GitLab