diff --git a/tlatools/src/tla2sany/semantic/Context.java b/tlatools/src/tla2sany/semantic/Context.java index a178f2ae58db10521d76f82dd2558eca9d5ffaf8..2181c5ce6096a1d550e4b748e33f8ecd87af5df7 100644 --- a/tlatools/src/tla2sany/semantic/Context.java +++ b/tlatools/src/tla2sany/semantic/Context.java @@ -241,7 +241,7 @@ public class Context implements ExploreNode { * Returns a Vector of those SymbolNodes in this Context that are * instances of class "template" (or one of its subclasses) */ - public Vector<SymbolNode> getByClass( Class template ) { + public Vector<SymbolNode> getByClass( Class<?> template ) { Vector<SymbolNode> result = new Vector<>(); Enumeration<Pair> list = table.elements(); while (list.hasMoreElements()) { @@ -360,72 +360,72 @@ public class Context implements ExploreNode { * The original implementation added the elements of Context ct to * this context in the inverse order as they appear in ct. It was * changed on 12 Mar 2013 by LL to add them in the same order. + * + * Note that the return value is never used in our code base. (2020.03.06) */ - public boolean mergeExtendContext(Context ct) { - boolean erc = true; - - // check locality, and multiplicity - // the .reversePairList was added to the following statement - // by LL on 12 Mar 2013 - Pair p = ct.lastPair.reversePairList(); - while (p != null) { - // Walk back along the list of pairs added to Context "ct" - SymbolNode sn = p.info; - - // Ignore local symbols in Context "ct" - if (!sn.isLocal()) { - Object sName; - if (sn instanceof ModuleNode) { - sName = new SymbolTable.ModuleName(sn.getName()); - } - else { - sName = sn.getName(); - } - - if (!table.containsKey(sName)) { - // If this context DOES NOT contain this name, add it: - table.put(sName, new Pair(sn)); - } - else { - // If this Context DOES contain this name - SymbolNode symbol = ((Pair)table.get(sName)).info; - if (symbol != sn) { - // if the two SymbolNodes with the same name are distinct nodes, - // We issue a warning or do nothing if they are instances of the same Java - // class--i.e. FormalParamNode, OpDeclNode, OpDefNode, or ModuleNode--doing - // nothing if they are both definitions coming from the same module. - // otherwise, it is considered to be an error. - // Option of doing nothing if from same module added by LL on 31 Oct 2012 to - // fix problem caused by the same module being both EXTENDed and imported with - // a LOCAL INSTANCE. Previously, it always added the warning. - if (symbol.getClass() == sn.getClass()) { - if (! symbol.sameOriginallyDefinedInModule(sn)) { - errors.addWarning( sn.getTreeNode().getLocation(), - "Warning: the " + kindOfNode(symbol) + " of '" + - sName.toString() + - "' conflicts with \nits " + kindOfNode(symbol) + " at " + - symbol.getTreeNode().getLocation() + "."); - } - } - else { - errors.addError( sn.getTreeNode().getLocation(), - "The " + kindOfNode(symbol) + " of '" + - sName.toString() + - "' conflicts with \nits " + kindOfNode(symbol) + " at " + - symbol.getTreeNode().getLocation() + "."); + public boolean mergeExtendContext(final Context ct) { + if (ct.lastPair == null) { + // If the context represents an inner module that defines no EXTENDS, ct.lastPair will be null + return true; + } + + boolean erc = true; + // check locality, and multiplicity + // the .reversePairList was added to the following statement + // by LL on 12 Mar 2013 + Pair p = ct.lastPair.reversePairList(); + while (p != null) { + // Walk back along the list of pairs added to Context "ct" + SymbolNode sn = p.info; + + // Ignore local symbols in Context "ct" + if (!sn.isLocal()) { + Object sName; + if (sn instanceof ModuleNode) { + sName = new SymbolTable.ModuleName(sn.getName()); + } else { + sName = sn.getName(); + } + + if (!table.containsKey(sName)) { + // If this context DOES NOT contain this name, add it: + table.put(sName, new Pair(sn)); + } else { + // If this Context DOES contain this name + SymbolNode symbol = ((Pair) table.get(sName)).info; + if (symbol != sn) { + // if the two SymbolNodes with the same name are distinct nodes, + // We issue a warning or do nothing if they are instances of the same Java + // class--i.e. FormalParamNode, OpDeclNode, OpDefNode, or ModuleNode--doing + // nothing if they are both definitions coming from the same module. + // otherwise, it is considered to be an error. + // Option of doing nothing if from same module added by LL on 31 Oct 2012 to + // fix problem caused by the same module being both EXTENDed and imported with + // a LOCAL INSTANCE. Previously, it always added the warning. + if (symbol.getClass() == sn.getClass()) { + if (!symbol.sameOriginallyDefinedInModule(sn)) { + errors.addWarning(sn.getTreeNode().getLocation(), + "Warning: the " + kindOfNode(symbol) + " of '" + sName.toString() + + "' conflicts with \nits " + kindOfNode(symbol) + " at " + + symbol.getTreeNode().getLocation() + "."); + } + } else { + errors.addError(sn.getTreeNode().getLocation(), + "The " + kindOfNode(symbol) + " of '" + sName.toString() + "' conflicts with \nits " + + kindOfNode(symbol) + " at " + symbol.getTreeNode().getLocation() + "."); // "Incompatible multiple definitions of symbol '" + // sName.toString() + // "'; \nthe conflicting declaration is at " + // symbol.getTreeNode().getLocation()+ "."); - erc = false; - } //end else - } // end if - } // end else - } - p = p.link; - } - return erc; + erc = false; + } // end else + } // end if + } // end else + } + p = p.link; + } + return erc; } private static String kindOfNode(SymbolNode symbol) { diff --git a/tlatools/test-model/Github429.tla b/tlatools/test-model/Github429.tla new file mode 100644 index 0000000000000000000000000000000000000000..8ad0cd5b51170b7d00c1998a5979b9f1e1957d3c --- /dev/null +++ b/tlatools/test-model/Github429.tla @@ -0,0 +1,14 @@ +---- MODULE Github429 ---- + +---- MODULE Alpha ---- + +====================== + +---- MODULE Beta ---- +EXTENDS Alpha + + +VARIABLE y +====================== + +================================== diff --git a/tlatools/test/tla2sany/drivers/Github429Test.java b/tlatools/test/tla2sany/drivers/Github429Test.java new file mode 100644 index 0000000000000000000000000000000000000000..f0508ac553f59356554a42341e95907faa92c127 --- /dev/null +++ b/tlatools/test/tla2sany/drivers/Github429Test.java @@ -0,0 +1,32 @@ +package tla2sany.drivers; + +import org.junit.Assert; +import org.junit.Before; +import org.junit.Test; + +import tla2sany.modanalyzer.SpecObj; +import util.SimpleFilenameToStream; +import util.ToolIO; + +public class Github429Test { + + private SpecObj moduleSpec; + + @Before + public void setUp() throws Exception { + // create a model and initialize + moduleSpec = new SpecObj("test-model/Github429.tla", new SimpleFilenameToStream()); + SANY.frontEndInitialize(moduleSpec, ToolIO.out); + } + + @Test + public void testForFailedParse() { + try { + SANY.frontEndParse(moduleSpec, ToolIO.out); + SANY.frontEndSemanticAnalysis(moduleSpec, ToolIO.out, false); + } catch (final Exception e) { + Assert.fail("No exception should occur during parse. Instead encountered [" + e.getClass() + + "] with message: " + e.getMessage()); + } + } +}