From f16da3762d5f4d6029d6fa48b2aa0c3ed987a7fc Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 3 Dec 2015 02:48:20 +0000
Subject: [PATCH] Add missing file from last commit.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10964 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/visitor/SemanticCheck.java | 74 +++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 prism/src/parser/visitor/SemanticCheck.java

diff --git a/prism/src/parser/visitor/SemanticCheck.java b/prism/src/parser/visitor/SemanticCheck.java
new file mode 100644
index 00000000..973e1faf
--- /dev/null
+++ b/prism/src/parser/visitor/SemanticCheck.java
@@ -0,0 +1,74 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package parser.visitor;
+
+import parser.ast.ExpressionFormula;
+import parser.ast.ExpressionFunc;
+import parser.ast.ExpressionIdent;
+import prism.PrismLangException;
+
+/**
+ * Perform any required semantic checks. These are just simple checks on expressions, mostly.
+ * For semantic checks on models and properties, specifically, see:
+ * {@link parser.visitor.ModulesFileSemanticCheck} and {@link parser.visitor.PropertiesSemanticCheck}. 
+ * These checks are done *before* any undefined constants have been defined.
+ */
+public class SemanticCheck extends ASTTraverse
+{
+	public SemanticCheck()
+	{
+	}
+
+	public void visitPost(ExpressionFunc e) throws PrismLangException
+	{
+		// Check function name is valid
+		if (e.getNameCode() == -1) {
+			throw new PrismLangException("Unknown function \"" + e.getName() + "\"", e);
+		}
+		// Check num arguments
+		if (e.getNumOperands() < e.getMinArity()) {
+			throw new PrismLangException("Not enough arguments to \"" + e.getName() + "\" function", e);
+		}
+		if (e.getMaxArity() != -1 && e.getNumOperands() > e.getMaxArity()) {
+			throw new PrismLangException("Too many arguments to \"" + e.getName() + "\" function", e);
+		}
+	}
+
+	public void visitPost(ExpressionIdent e) throws PrismLangException
+	{
+		// By the time the expression is checked, this should
+		// have been converted to an ExpressionVar/ExpressionConstant/...
+		throw new PrismLangException("Undeclared identifier", e);
+	}
+
+	public void visitPost(ExpressionFormula e) throws PrismLangException
+	{
+		// This should have been defined or expanded by now
+		if (e.getDefinition() == null)
+			throw new PrismLangException("Unexpanded formula", e);
+	}
+}