Commit 8a961adf authored Oct 18, 2014 by Matthew Dawson

Verify in decrementLevel in the *Parser classes never over decrements.

decrementLevel should never cause m_level to go below 0.  This ensures a
bug in ANTLR won't cause random NPE's elsewhere in the code.

parent 25e839da

src/main/java/ca/mcscert/jtet/parsers/MatlabParser.java

+6 −0

Original line number	Diff line number	Diff line
		@@ -88,6 +88,12 @@ final public class MatlabParser {

		private void decrementLevel() {
		this.m_level--;
		if (this.m_level < 0) {
		// This can only happen if ANTLR manages to exit more E* states then enters (which should never happen,
		// even if a given expression is invalid!
		throw new IllegalStateException("Decremented more levels then incremeted");
		}

		if (!m_hiddenOpStack.isEmpty() && m_hiddenOpStack.peekFirst().level == m_level) {
		// We have a hidden op here. The normal methods won't find it, so make use of it!
		HiddenOpStackContainer hiddenOp = m_hiddenOpStack.peekFirst();

src/main/java/ca/mcscert/jtet/parsers/PVSSimpleParser.java

+6 −0

Original line number	Diff line number	Diff line
		@@ -90,6 +90,12 @@ final public class PVSSimpleParser {

		private void decrementLevel() {
		this.m_level--;
		if (this.m_level < 0) {
		// This can only happen if ANTLR manages to exit more E* states then enters (which should never happen,
		// even if a given expression is invalid!
		throw new IllegalStateException("Decremented more levels then incremeted");
		}

		if (!m_hiddenOpStack.isEmpty() && m_hiddenOpStack.peekFirst().level == m_level) {
		// We have a hidden op here. The normal methods won't find it, so make use of it!
		HiddenOpStackContainer hiddenOp = m_hiddenOpStack.peekFirst();