Skip to content
Snippets Groups Projects
Commit ad4ce613 authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

Do not warn on an unmatched operators if Java overrides disabled

warnings.

[Refactor][TLC]
parent 1c920e11
No related branches found
No related tags found
No related merge requests found
...@@ -61,4 +61,12 @@ public @interface Evaluation { ...@@ -61,4 +61,12 @@ public @interface Evaluation {
* @see tlc2.tool.impl.SpecProcessor.processConstantDefns() * @see tlc2.tool.impl.SpecProcessor.processConstantDefns()
*/ */
int minLevel() default 0; 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;
} }
...@@ -52,4 +52,9 @@ public @interface TLAPlusOperator { ...@@ -52,4 +52,9 @@ public @interface TLAPlusOperator {
* @see tlc2.overrides.Evaluation.minLevel() * @see tlc2.overrides.Evaluation.minLevel()
*/ */
int minLevel() default 0; int minLevel() default 0;
/**
* @return tlc2.overrides.Evaluation.warn()
*/
boolean warn() default true;
} }
...@@ -589,15 +589,14 @@ public class SpecProcessor implements ValueConstants, ToolGlobals { ...@@ -589,15 +589,14 @@ public class SpecProcessor implements ValueConstants, ToolGlobals {
final ModuleNode moduleNode = modSet.get(evaluation.module()); final ModuleNode moduleNode = modSet.get(evaluation.module());
if (moduleNode == null) { if (moduleNode == null) {
// If the module, for which the operator has been defined, isn't part of the spec, if (evaluation.warn()) MP.printMessage(EC.TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_MODULE_MISMATCH,
// it is probably intentional and thus confusing to warn the user. This e.g. evaluation.module() + "!" + evaluation.definition(),
// happen with CommunitModules which has a bunch of operators spread over a set c.getResource(c.getSimpleName() + ".class").toExternalForm(), val.toString());
// modules and a user only uses a subset in her spec.
continue LOOP; continue LOOP;
} }
final OpDefNode opDef = moduleNode.getOpDef(evaluation.definition()); final OpDefNode opDef = moduleNode.getOpDef(evaluation.definition());
if (opDef == null) { 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(), evaluation.module() + "!" + evaluation.definition(),
c.getResource(c.getSimpleName() + ".class").toExternalForm(), val.toString()); c.getResource(c.getSimpleName() + ".class").toExternalForm(), val.toString());
continue LOOP; continue LOOP;
...@@ -619,24 +618,24 @@ public class SpecProcessor implements ValueConstants, ToolGlobals { ...@@ -619,24 +618,24 @@ public class SpecProcessor implements ValueConstants, ToolGlobals {
if (opOverrideCandidate != null) { if (opOverrideCandidate != null) {
final ModuleNode moduleNode = modSet.get(opOverrideCandidate.module()); final ModuleNode moduleNode = modSet.get(opOverrideCandidate.module());
if (moduleNode == null) { 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()); opOverrideCandidate.identifier(), opOverrideCandidate.module(), m.toString());
continue LOOP; continue LOOP;
} }
final OpDefNode opDef = moduleNode.getOpDef(opOverrideCandidate.identifier()); final OpDefNode opDef = moduleNode.getOpDef(opOverrideCandidate.identifier());
if (opDef == null) { 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()); opOverrideCandidate.identifier(), opOverrideCandidate.module(), m.toString());
continue LOOP; continue LOOP;
} }
final Value val = MethodValue.get(m, opOverrideCandidate.minLevel()); final Value val = MethodValue.get(m, opOverrideCandidate.minLevel());
if (opDef.getArity() != m.getParameterCount()) { 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()); opDef.getName().toString(), c.getName(), val.toString());
continue LOOP; continue LOOP;
} else { } 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(), opDef.getName().toString(), c.getName(),
val instanceof MethodValue ? val.toString() : val.getClass().getName()); // toString of non-MethodValue instances can be expensive. val instanceof MethodValue ? val.toString() : val.getClass().getName()); // toString of non-MethodValue instances can be expensive.
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment