TreeParser.java

/**
 * This class processes the parse tree created by the ANTLR parser and
 * construct the front-end AST.
 * 
 * Please find the complete language grammar in MiniMP.g which locates in the same directory.
 * author: Yi Wei
 */

package edu.udel.cis.vsl.tass.front.minimp.parser;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.util.Collection;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Stack;
import java.util.Vector;

import org.antlr.runtime.ANTLRFileStream;
import org.antlr.runtime.CharStream;
import org.antlr.runtime.CommonTokenStream;
import org.antlr.runtime.RecognitionException;
import org.antlr.runtime.Token;
import org.antlr.runtime.tree.CommonTree;

import edu.udel.cis.vsl.tass.config.CompareConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.config.VerifyConfiguration;
import edu.udel.cis.vsl.tass.front.FrontendIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTAbstractFunctionDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTArrayHeader;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTArrayVariableDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTDeclarationIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTFormalParameterDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTFunctionDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTSimpleVariableDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTStructVariableDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTSystemFunctionDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTVariableDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTVariableDeclaration.VariableCategory;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTAddressOfExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTArrayLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTArraySubscriptExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTAssignExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTBinaryExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTBoolLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTBufferExpressionIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTCharLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTConstantExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTDereferenceExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTEvaluatedFunction;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTExpressionIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTIfThenElseExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTIntegerLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTLhsArraySubscriptExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTLhsExpressionIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTLhsStructMemberRefExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTLhsVariableExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTLiteralExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTNullLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTQuantifierExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTRealLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSelfChangeExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSizeofExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSpecExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTStructLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTStructMemberRefExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSystemVariable;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTTypeCast;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTUnaryExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTVariableExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTWildcardExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTBinaryExpression.BinaryOperator;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTQuantifierExpression.QuantifierKind;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSelfChangeExpression.SelfChangeOperator;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSystemVariable.SYS_VAR;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTUnaryExpression.UnaryOperator;
import edu.udel.cis.vsl.tass.front.minimp.ast.misc.AST;
import edu.udel.cis.vsl.tass.front.minimp.ast.misc.ASTFunction;
import edu.udel.cis.vsl.tass.front.minimp.ast.misc.ASTIdentifier;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTAllocateStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTAssertStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTAssignmentStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTAssumeStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTCompoundStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTConditionStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTEmptyStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTForStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTInvocationStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTLoopInvariant;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTReceiveStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTReturnStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTSelectStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTSelection;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTSendStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTStatementIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTWhileStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTArrayType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTBoolType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTCharType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTIntegerType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTPointerType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTRealType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTScalarType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTStructType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTTypeIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTUnknownType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTVoidType;
import edu.udel.cis.vsl.tass.front.minimp.lib.LibraryIF;
import edu.udel.cis.vsl.tass.front.minimp.lib.LibraryLoader;
import edu.udel.cis.vsl.tass.model.IF.SyntaxException;
import edu.udel.cis.vsl.tass.util.Source;

public class TreeParser implements FrontendIF {
	// Abstract syntax tree built by ANTLR parser
	private CommonTree ast;
	// Source program file.
	private File file;

	private LibraryLoader libraryLoader = new LibraryLoader();

	private Collection<String> libraryNames = new LinkedHashSet<String>();

	private LinkedHashMap<String, ASTDeclarationIF> globalVariableMap;

	private LinkedHashMap<String, ASTExpressionIF> constantMap = new LinkedHashMap<String, ASTExpressionIF>();

	// All global variables will be added to this list according to the order
	// they are declared.
	private Vector<ASTDeclarationIF> globalVariableList;

	private Vector<ASTFunctionDeclaration> functionList;
	private Vector<ASTAbstractFunctionDeclaration> abstractFunctionList;

	// Indicate whether the parser is processing global variables.
	private boolean isProcessingGlobalVar = true;

	// Determine whether the parser is processing function declaration now
	private boolean isProcessingFunction = false;

	// Determine whether the parser is processing a reference to a spec variable
	private boolean isProcessingSpecVar = false;

	private Map<String, ASTDeclarationIF> localVariableMap;

	private Map<String, ASTDeclarationIF> boundVariableMap;

	// Global variable to store array dimensions
	private ASTArrayHeader arrayHeader = null;

	// Configuration of TASS execution.
	private RunConfiguration configuration = null;

	// Used in the situation that multiple language elements requires source to
	// be set.
	private Source lastPosition = null;

	// This table is used to look up the alias type names
	private LinkedHashMap<String, ASTTypeIF> typeNameMap;

	// This table is used to store user defined types
	private LinkedHashMap<String, ASTTypeIF> typeTable;

	// For processing dimensions in array type variables
	private Stack<ASTExpressionIF> dimensionStack;

	// The following three fields are used to facilitate processing loop
	// joint-invariants
	private AST specProgram;

	// Current function for the program that is being processed.
	private ASTIdentifier currentFunction = null;

	private ASTIdentifier specFunction = null;

	// The following two fields are for processing initializers
	private Stack<ASTExpressionIF> indexStack;

	private int minDepth = -1;
	private int designatorCount = 0;
	private boolean firstInitList = true;
	private boolean isInDifferentList = false;

	// Ditto
	private boolean hasProcessedDesignation = false;

	// For processing array variable or array operations.
	private Vector<Integer> dimensionList = null;

	// Ditto
	private Vector<Integer> indexList = null;

	// A flag for increase/decrease the index stack in variable initializer
	// processing.
	private boolean fromInitializer = false;

	// Store the last line and column when extracting source code information.
	private int lastLine = 0;
	private int lastColumn = 0;

	// Keep a struct type for referencing variables in other processes using
	// PROC[pid].variable
	private ASTStructType procArrayStructType = null;

	// For array initialization
	private ASTArrayLiteral arrayLiteral = null;
	private ASTStructLiteral structLiteral = null;

	public TreeParser(RunConfiguration configuration, AST specProgram)
			throws IOException {
		this.configuration = configuration;
		this.specProgram = specProgram;

	}

	public TreeParser(String fileName, RunConfiguration configuration,
			AST specProgram) throws IOException, SyntaxException {

		this(configuration, specProgram);
		if ((System.getProperty("tass.library.path") + "/libstdlib.c")
				.equals(fileName)) {
			ASTPointerType voidPointerType = new ASTPointerType(
					new ASTVoidType());

			constantMap.put("NULL", new ASTConstantExpression("NULL",
					new ASTNullLiteral(voidPointerType), voidPointerType));
		}
		prepareFile(fileName);
	}

	public TreeParser(VerifyConfiguration configuration) {
		this.configuration = configuration;
	}

	@Override
	public AST processAST(File modelFile) throws SyntaxException, IOException {
		String fileName = modelFile.getAbsolutePath();
		prepareFile(fileName);
		return processAST();
	}

	private void prepareFile(String fileName) throws SyntaxException,
			IOException {
		// Using the generated lexer and parser to build the AST.
		CharStream input = null;
		input = new ANTLRFileStream(fileName);
		MiniMPLexer lex = new MiniMPLexer(input);
		CommonTokenStream tokens = new CommonTokenStream(lex);
		MiniMPParser parser = new MiniMPParser(tokens);
		MiniMPParser.program_return r = null;
		try {
			r = parser.program();
		} catch (RecognitionException e) {
			throw new SyntaxException(parser.getSourceName()
					+ " parsed unsuccessfully: \n" + e.getMessage());
		}
		// Get the number of syntax errors from the lexer/parser.
		int errors = parser.getNumberOfSyntaxErrors();
		if (errors > 0) {
			throw new SyntaxException(parser.getSourceName()
					+ " parsed unsuccessfully.");
		}
		file = new File(fileName);
		this.ast = (CommonTree) r.tree;
	}

	/**
	 * Process the AST generated by Antlr, returns a well organized program
	 * object.
	 */
	public AST processAST() throws SyntaxException {
		Token root = ast.getToken();
		this.globalVariableMap = new LinkedHashMap<String, ASTDeclarationIF>();
		this.functionList = new Vector<ASTFunctionDeclaration>();
		this.abstractFunctionList = new Vector<ASTAbstractFunctionDeclaration>();
		this.globalVariableList = new Vector<ASTDeclarationIF>();
		this.typeNameMap = new LinkedHashMap<String, ASTTypeIF>();
		this.typeTable = new LinkedHashMap<String, ASTTypeIF>();

		ASTIdentifier procID = new ASTIdentifier("PROC");
		procArrayStructType = new ASTStructType();
		int numProcs = 1;
		if (configuration instanceof VerifyConfiguration) {
			numProcs = ((VerifyConfiguration) configuration).numProcs();
		} else if (specProgram != null) {
			// This is an impl
			numProcs = ((CompareConfiguration) configuration).implNumProcs();
		} else {
			// This is a spec
			numProcs = ((CompareConfiguration) configuration).specNumProcs();
		}
		ASTArrayHeader procArrayHeader = new ASTArrayHeader(new ASTArrayType(
				procArrayStructType), new ASTIntegerLiteral(numProcs));
		ASTDeclarationIF procArrayDecl = new ASTArrayVariableDeclaration(
				procID, procArrayHeader, VariableCategory.PROCESS);
		globalVariableMap.put("PROC", procArrayDecl);
		globalVariableList.add(procArrayDecl);
		// MiniMPLexer.PROGRAM is the root of an AST.
		if (root.getType() != MiniMPLexer.PROGRAM) {
			reportSyntaxException(
					"Expected MiniMPLexer.PROGRAM as the root of the AST, instead got "
							+ root.getType(), 1, 1);
		}

		// Process variable, type or function declarations.
		for (int i = 0; i < ast.getChildCount(); i++) {
			CommonTree child = (CommonTree) (ast.getChild(i));
			if (child.getType() == MiniMPLexer.INCLUDE_DIRECTIVE) {
				processInclude(child);
			} else if (child.getType() == MiniMPLexer.DEFINE_DIRECTIVE) {
				processDefine(child);
			} else if (child.getType() == MiniMPLexer.DECLARATION
					|| child.getType() == MiniMPLexer.MULTI_DECLARATION) {
				if (this.isProcessingGlobalVar == false) {
					this.isProcessingGlobalVar = true;
				}
				processDeclaration(child);
			} else if (child.getType() == MiniMPLexer.FUNCTION_DECL) {
				if (this.isProcessingGlobalVar == true) {
					this.isProcessingGlobalVar = false;
				}
				if (this.isProcessingFunction == false) {
					this.isProcessingFunction = true;
				}
				ASTFunctionDeclaration function = processFunction(child);
				/* If the function is a prototype, it will return null.  We don't need
				 *  to do anything in that case.
				 */
				if (function != null) {
					function = checkReturn(function, child);
					this.functionList.add(function);
				}
			} else if (child.getType() == MiniMPLexer.ABSTR_FUNCTION_DECL) {
				if (this.isProcessingGlobalVar == true) {
					this.isProcessingGlobalVar = false;
				}
				ASTAbstractFunctionDeclaration function = processAbstractFunction(child);
				this.abstractFunctionList.add(function);
				globalVariableMap.put(function.getName().toString(), function);
			}
		}
		return new AST(libraryNames, this.globalVariableMap,
				this.globalVariableList, this.functionList,
				this.abstractFunctionList, this.typeNameMap, this.constantMap);
	}

	private void processDefine(CommonTree node) throws SyntaxException {
		assert node.getType() == MiniMPLexer.DEFINE_DIRECTIVE;
		assert node.getChildCount() == 2;
		ASTIdentifier id = processID((CommonTree) node.getChild(0));
		ASTExpressionIF value = processExpr((CommonTree) node.getChild(1));
		ASTExpressionIF constant = new ASTConstantExpression(id
				.source().text(), value, value.getType());
		Source src = this.getSourcePos((CommonTree) (node
				.getChild(0)), (CommonTree) (node.getChild(node
				.getChildCount() - 1)));
		constant.setSource(src);
		constantMap.put(id.source().text(), constant);

	}

	private void processInclude(CommonTree node) throws SyntaxException {
		assert node.getType() == MiniMPLexer.INCLUDE_DIRECTIVE;
		assert node.getChildCount() == 1;

		String name = node.getChild(0).getText().substring(1);
		int index = name.indexOf('<');
		if (index == -1)
			index = name.indexOf("\"");
		int lastIndex = name.lastIndexOf('>');
		if (lastIndex == -1)
			lastIndex = name.lastIndexOf("\"");
		name = name.substring(index + 1, lastIndex);
		// TODO process <> and "" differently.
		libraryNames.add(name);

		// the following opens the library file, parses it,
		// and populates the fields in the library object:
		LibraryIF library = libraryLoader.loadLibrary(null, name);

		// the following iterates over the fields of the library object
		// and adds those items to the main AST:
		
		// transitive closure: include all libraries used by
		// the included library...
		libraryNames.addAll(library.getLibrariesUsed());
		
		for (String typeName : library.getTypes().keySet()) {

			// report type name redefinition error
			if (this.typeNameMap.containsKey(typeName)) {
				throw new SyntaxException(this.typeNameMap.get(typeName),
						"Redefinition of type " + typeName);
			} else {
				// Get the base type
				ASTTypeIF baseType = library.getTypes().get(typeName);
				// process chain typedefs
				if (baseType instanceof ASTUnknownType) {
					String possibleTypeName = ((ASTUnknownType) baseType)
							.getName();
					if (this.typeNameMap.containsKey(possibleTypeName)) {
						baseType = this.typeNameMap.get(possibleTypeName);
					} else {
						this.reportSyntaxException(
								"Data definition has no type.", node.getLine(),
								node.getCharPositionInLine());
					}
				}
				// Add the new alternate type name to the map
				this.typeNameMap.put(typeName, baseType);
			}
		}
		for (ASTVariableDeclaration decl : library.getInputs()) {
			if (decl.getName().toString().equals("PROC")) {
				for (int j = 0; j < ((ASTStructType) ((ASTArrayType) decl
						.getType()).getBaseType()).numFieldTypes(); j++) {
					procArrayStructType.addFieldType(
							((ASTStructType) ((ASTArrayType) decl.getType())
									.getBaseType()).getFieldName(j),
							((ASTStructType) ((ASTArrayType) decl.getType())
									.getBaseType()).getFieldType(j));
				}
			} else {
				this.globalVariableMap.put(decl.getName().toString(), decl);
				this.globalVariableList.add(decl);
			}
		}
		for (String constantName : library.getConstants().keySet()) {
			if (constantMap.containsKey(constantName)) {
				// throw new SyntaxException(null,
				// "Redefinition of constant "
				// + constantName);
			}
			constantMap.put(constantName,
					library.getConstants().get(constantName));
		}

	}

	private void processDeclarationList(CommonTree node) throws SyntaxException {
		for (int i = 0; i < node.getChildCount(); i++) {
			processDeclaration((CommonTree) (node.getChild(i)));
		}
	}

	private void processDeclaration(CommonTree node) throws SyntaxException {
		VariableCategory kind = VariableCategory.PROCESS;
		if (node.getChild(0).getType() == MiniMPLexer.PREFIX) {
			// A typedef declaration
			String prefix = node.getChild(0).getChild(0).getText();
			if (prefix.equals("typedef")) {
				processDeclarationBody((CommonTree) (node.getChild(1)), true,
						VariableCategory.TYPEDEF);
			} else {
				// Non global declarations can only use typedef as prefix.
				if (this.isProcessingGlobalVar == false) {
					this.reportSyntaxException(
							"Non-global declarations can not use input/output/shared as prefix.",
							node.getLine(), node.getCharPositionInLine());
				} else {
					// Process different types of global variables.
					if (prefix.equals("input")) {
						kind = VariableCategory.INPUT;
					} else if (prefix.equals("output")) {
						kind = VariableCategory.OUTPUT;
					} else if (prefix.equals("shared")) {
						kind = VariableCategory.SHARED;
					} else {
						this.reportSyntaxException(
								"Unrecognized declaration prefix " + prefix,
								node.getChild(0).getLine(), node.getChild(0)
										.getCharPositionInLine());
					}
					ASTDeclarationIF declBody = processDeclarationBody(
							(CommonTree) (node.getChild(1)), false, kind);
					if (declBody == null) {
						return;
					}
					((ASTVariableDeclaration) declBody)
							.setVariableCategory(kind);
					if (this.isProcessingGlobalVar) {
						this.globalVariableMap.put(declBody.getName()
								.toString(), declBody);
						this.globalVariableList.add(declBody);
					} else {
						this.localVariableMap.put(
								declBody.getName().toString(), declBody);
					}

					// process suffix
					if (node.getChild(node.getChildCount() - 2).getType() == MiniMPLexer.SUFFIX) {
						CommonTree suffix = (CommonTree) (node.getChild(node
								.getChildCount() - 2));
						// process assumptions
						if (suffix.getChild(0).getType() == MiniMPLexer.EXPR) {
							if (kind != VariableCategory.INPUT) {
								this.reportSyntaxException(
										"Only input variables can have initial assumptions.",
										suffix.getLine(),
										suffix.getCharPositionInLine());
							} else {
								ASTExpressionIF assumption = this
										.processExpr((CommonTree) (suffix
												.getChild(0)));
								((ASTVariableDeclaration) declBody)
										.setAssumption(assumption);
								// Has corresponding variable
								if (suffix.getChildCount() == 3) {
									if (kind == VariableCategory.INPUT
											|| kind == VariableCategory.OUTPUT) {
										ASTIdentifier id = this
												.processID((CommonTree) (suffix
														.getChild(2)));
										((ASTVariableDeclaration) declBody)
												.setCorrespondence(id);
									} else {
										this.reportSyntaxException(
												"Only input or output variables can have corresponding variables.",
												suffix.getLine(),
												suffix.getCharPositionInLine());
									}
								}
							}
						}
						// Only have corresponding variables
						else {
							if (kind == VariableCategory.INPUT
									|| kind == VariableCategory.OUTPUT) {
								ASTIdentifier id = this
										.processID((CommonTree) (suffix
												.getChild(0)));
								((ASTVariableDeclaration) declBody)
										.setCorrespondence(id);
							} else {
								this.reportSyntaxException(
										"Only input or output variables can have corresponding variables.",
										suffix.getLine(),
										suffix.getCharPositionInLine());
							}
						}
					}
					Source src = this.getSourcePos((CommonTree) (node
							.getChild(0)), (CommonTree) (node.getChild(node
							.getChildCount() - 1)));
					declBody.setSource(src);
					declBody.setText(this.extractSource(src));
				}
			}
		} else if (node.getType() == MiniMPLexer.MULTI_DECLARATION) {
			// Multiple variables declared on the same line are handled like a
			// declaration list
			for (int i = 0; i < node.getChildCount(); i++) {
				processDeclaration((CommonTree) (node.getChild(i)));
			}
		} else {
			// A variable other than an input or a output variable can not have
			// suffix
			if (node.getChildCount() == 3) {
				this.reportSyntaxException(
						"A variable other than input or output variable can not have suffix",
						node.getLine(), node.getCharPositionInLine());
			} else {
				if (this.isProcessingGlobalVar) {
					kind = VariableCategory.PROCESS;
				} else {
					kind = VariableCategory.LOCAL;
				}
				ASTDeclarationIF decl = processDeclarationBody(
						(CommonTree) (node.getChild(0)), false, kind);
				if (decl == null) {
					return;
				}
				Source src = getSourcePos((CommonTree) (node.getChild(0)),
						(CommonTree) (node.getChild(node.getChildCount() - 1)));
				decl.setSource(src);
				decl.setText(extractSource(src));
				if (this.isProcessingGlobalVar) {
					this.globalVariableMap.put(decl.getName().toString(), decl);
					this.globalVariableList.add(decl);
					procArrayStructType.addFieldType(decl.getName().toString(),
							decl.getType());
				} else {
					String refName = decl.getName().toString() + "@"
							+ currentFunction.toString();
					procArrayStructType.addFieldType(refName, decl.getType());
					this.localVariableMap.put(decl.getName().toString(), decl);
				}
			}
		}
	}

	// NOTE: isTypedef is not used anywhere!

	private ASTDeclarationIF processDeclarationBody(CommonTree node,
			boolean isTypedef, VariableCategory kind) throws SyntaxException {
		// declaration_body: typename
		if (node.getChildCount() == 1) {
			processTypeSpecifier((CommonTree) (node.getChild(0)));
			return null;
		}
		// process base type
		ASTTypeIF baseType = this.processTypeSpecifier((CommonTree) (node
				.getChild(0)));
		// process chain typedefs
		if (baseType instanceof ASTUnknownType) {
			String possibleTypeName = ((ASTUnknownType) baseType).getName();
			if (this.typeNameMap.containsKey(possibleTypeName)) {
				baseType = this.typeNameMap.get(possibleTypeName);
			} else {
				this.reportSyntaxException("Data definition has no type.", node
						.getChild(0).getLine(), node.getChild(0)
						.getCharPositionInLine());
			}
		}

		NameTypePair pair = this.processDeclarator(
				(CommonTree) (node.getChild(1)), baseType);
		// typedef declaration
		if (kind == VariableCategory.TYPEDEF) {
			if (node.getChildCount() == 3) {
				this.reportSyntaxException(
						"A typedef declaration can not have initializer.",
						node.getLine(), node.getCharPositionInLine());
			}
			// report type name redefinition error
			if (this.typeNameMap.containsKey(pair.getName())) {
				this.reportSyntaxException(
						"Redefinition of type " + pair.getName(), node
								.getChild(1).getLine(), node.getChild(1)
								.getCharPositionInLine());
			} else {
				// Add the new alternate type name to the map
				this.typeNameMap.put(pair.getName().toString(), pair.getType());
				return null;
			}
		}
		// normal declaration
		else {
			ASTVariableDeclaration result = null;
			// Array type variable
			if (pair.getType() instanceof ASTArrayType) {
				// Note: The second argument is a class-wide variable, make sure
				// to reset it after using it.
				if (this.arrayHeader == null) {
					throw new edu.udel.cis.vsl.tass.model.IF.SyntaxException(
							pair.getName().source(), "Header can not be null.");
				}
				result = new ASTArrayVariableDeclaration(pair.getName(),
						this.arrayHeader, kind);
				this.arrayHeader = null;
			} else if (pair.getType() instanceof ASTStructType) {
				result = new ASTStructVariableDeclaration(pair.getName(),
						pair.getType(), kind);
			} else if (pair.getType() instanceof ASTScalarType
					|| pair.getType() instanceof ASTPointerType) {
				result = new ASTSimpleVariableDeclaration(pair.getName(),
						pair.getType(), kind);
			} else {
				this.reportSyntaxException(pair.getType()
						+ " can not be used as a variable type.",
						node.getLine(), node.getCharPositionInLine());
			}
			if (node.getChildCount() == 3) {
				// Create an "empty" array or struct literal to store the
				// initialization.
				if (result.getType() instanceof ASTArrayType
						|| result.getType() instanceof ASTStructType) {
					this.dimensionList = new Vector<Integer>();
					this.indexList = new Vector<Integer>();
					this.indexStack = new Stack<ASTExpressionIF>();
					ASTTypeIF temp = result.getType();
					while (temp instanceof ASTArrayType) {
						ASTExpressionIF dimension = ((ASTArrayType) temp)
								.getLength();
						if (!(dimension instanceof ASTIntegerLiteral)) {
							this.reportSyntaxException(
									"Variable length array can not have initializer.",
									node.getLine(),
									node.getCharPositionInLine());
						}
						Integer dimensionInfo = Integer
								.valueOf(((ASTIntegerLiteral) dimension)
										.getValue());
						this.dimensionList.add(dimensionInfo);
						temp = ((ASTArrayType) temp).getBaseType();
					}
					if (result.getType() instanceof ASTArrayType) {
						Integer[] dimensions = new Integer[this.dimensionList
								.size()];
						dimensionList.toArray(dimensions);
						this.arrayLiteral = new ASTArrayLiteral(
								result.getType(), dimensions);
					} else {
						this.structLiteral = new ASTStructLiteral(
								result.getType());
					}
				}

				ASTExpressionIF initializer = this.processInitializer(
						(CommonTree) (node.getChild(2)), result.getType());

				if (initializer == null) {
					if (this.arrayLiteral != null) {
						initializer = this.arrayLiteral;
					} else {
						initializer = this.structLiteral;
					}
				}
				// Cast integers to reals when they are the right side of a real declaration
				if (result.getType() instanceof ASTRealType && initializer instanceof ASTIntegerLiteral) {
					initializer = new ASTRealLiteral(initializer.toString());
				}
				result.setInit(initializer);
				this.indexList = null;
				this.indexStack = null;
				this.dimensionList = null;
				this.arrayLiteral = null;
				this.structLiteral = null;
				this.designatorCount = 0;
				this.minDepth = -1;
				this.firstInitList = true;
				this.isInDifferentList = false;
			}
			return result;
		}

		// ! The execution should never reach here.
		return null;
	}

	private ASTTypeIF processTypeSpecifier(CommonTree node)
			throws SyntaxException {
		Source source = this.getSourcePos(node, node);
		if (node.getChild(0).getType() == MiniMPLexer.SIMPLE_TYPE) {
			ASTTypeIF result = processSimpleType((CommonTree) (node.getChild(0)));
			result.setSource(source);
			return result;
		}
		// The "real" type referred by this id must be known before it can be
		// used.
		/*
		 * For example, in C, the following code snippet is legal typedef int A;
		 * typedef A B;
		 * 
		 * But the following one is illegal: typedef A B; typedef int A;
		 * 
		 * The MiniMP language also complies with the above rule.
		 */
		else if (node.getChild(0).getType() == MiniMPLexer.IDENTIFIER) {
			String name = this.processID((CommonTree) (node.getChild(0)))
					.toString();
			if (this.typeNameMap.containsKey(name)) {
				return this.typeNameMap.get(name);
			} else {
				this.reportSyntaxException("Type name " + name
						+ " has no type associated to it.", node.getChild(0)
						.getLine(), node.getChild(0).getCharPositionInLine());
			}
		}
		// Struct type
		else {
			// A struct can have a name or be anonymous
			ASTStructType result = null;
			// A reference to a defined struct type, like "struct A" in
			// "struct A a;"
			if (node.getChildCount() == 2
					&& node.getChild(1).getType() == MiniMPLexer.IDENTIFIER) {
				String name = this.processID((CommonTree) (node.getChild(1)))
						.toString();
				String key = "struct " + name;
				if (this.typeTable.containsKey(key)) {
					return this.typeTable.get(key);
				} else {
					this.reportSyntaxException("Type " + key
							+ " has incomplete type.", node.getLine(),
							node.getCharPositionInLine());
				}
			} else {
				// Indicate whether this is a named struct or an anonymous
				// struct.
				boolean hasName = true;
				String structName = "";
				int fieldStartIndex = 2;

				// An anonymous struct
				if (node.getChild(1).getType() != MiniMPLexer.IDENTIFIER) {
					hasName = false;
					fieldStartIndex = 1;
				} else {
					structName = this
							.processID((CommonTree) (node.getChild(1)))
							.toString();
				}

				if (hasName) {
					result = new ASTStructType(structName);
					this.typeTable.put(result.toString(), result);
				} else {
					result = new ASTStructType();
				}

				for (int i = fieldStartIndex; i < node.getChildCount(); i++) {
					NameTypePair field = this
							.processFieldDeclaration((CommonTree) (node
									.getChild(i)));
					if (this.arrayHeader != null) {
						this.arrayHeader = null;
					}
					String key = field.getName().toString();
					// duplicate field name
					if (result.hasField(key)) {
						this.reportSyntaxException(
								"Duplicate field declaration: " + key, node
										.getChild(i).getLine(), node
										.getChild(i).getCharPositionInLine());
					} else {
						result.addFieldType(key, field.getType());
					}
				}
			}
			return result;
		}
		// The execution should never reach here !
		return null;
	}

	private ASTTypeIF processSimpleType(CommonTree node) throws SyntaxException {
		String typeText = node.getChild(0).getText();
		if (typeText.equals("boolean")) {
			return new ASTBoolType();
		} else if (typeText.equals("int")) {
			return new ASTIntegerType();
		} else if (typeText.equals("float") || typeText.equals("double")) {
			return new ASTRealType();
		} else if (typeText.equals("char")) {
			return new ASTCharType();
		} else if (typeText.equals("void")) {
			return new ASTVoidType();
		} else {
			this.reportSyntaxException("Unrecognized type " + typeText, node
					.getChild(0).getLine(), node.getChild(0)
					.getCharPositionInLine());
		}
		// The execution should never reach here !
		return null;
	}

	private ASTTypeIF processTypeName(CommonTree node) throws SyntaxException {
		ASTTypeIF baseType = this.processTypeSpecifier((CommonTree) (node
				.getChild(0)));
		if (node.getChildCount() == 1) {
			return baseType;
		} else {
			return this.processAbstractDeclarator(
					(CommonTree) (node.getChild(1)), baseType);
		}
	}

	private ASTTypeIF processAbstractDeclarator(CommonTree node,
			ASTTypeIF baseType) throws SyntaxException {
		ASTTypeIF result = baseType;

		if (node.getChildCount() > 0) {
			int i = 0;
			// pointer type
			if (node.getChild(0).getText().equals("*")) {
				while (i < node.getChildCount()
						&& node.getChild(i).getText().equals("*")) {
					result = new ASTPointerType(result);
					i++;
				}
			}

			// direct abstract declarator
			if (i < node.getChildCount()
					&& node.getChild(i).getType() == MiniMPLexer.DIRECT_ABSTRACT_DECLARATOR) {
				// process the array part first
				int j = i;
				i++;

				this.dimensionStack = new Stack<ASTExpressionIF>();
				for (; i < node.getChildCount(); i++) {
					this.dimensionStack = new Stack<ASTExpressionIF>();
					result = this.processDeclaratorSuffix(
							(CommonTree) (node.getChild(i)), result, true);
				}

				if (!this.dimensionStack.empty()) {
					ASTTypeIF headerType = result;
					while (headerType instanceof ASTArrayType) {
						headerType = ((ASTArrayType) headerType).getBaseType();
					}
					while (!this.dimensionStack.empty()) {
						headerType = new ASTArrayType(headerType,
								this.dimensionStack.peek());
						ASTArrayHeader temp = new ASTArrayHeader(headerType,
								this.dimensionStack.pop());
						temp.setElementType(this.arrayHeader);
						this.arrayHeader = temp;
					}
					result = headerType;
				}
				// process the whole abstract declarator
				result = this.processDirectAbstractDeclarator(
						(CommonTree) (node.getChild(j)), result);
			}

			return result;
		}
		// Program should never reach here.
		return null;
	}

	private ASTTypeIF processDirectAbstractDeclarator(CommonTree node,
			ASTTypeIF baseType) throws SyntaxException {
		return this.processAbstractDeclarator((CommonTree) (node.getChild(1)),
				baseType);
	}

	private NameTypePair processFieldDeclaration(CommonTree node)
			throws SyntaxException {
		ASTTypeIF baseType = this.processTypeSpecifier((CommonTree) (node
				.getChild(0)));
		NameTypePair field = this.processDeclarator(
				(CommonTree) (node.getChild(1)), baseType);
		return field;
	}

	private NameTypePair processDeclarator(CommonTree node, ASTTypeIF baseType)
			throws SyntaxException {
		// No pointer
		if (node.getChildCount() == 1) {
			return this.processDirectDeclarator(
					(CommonTree) (node.getChild(0)), baseType);
		}
		// Process pointer type
		else {
			ASTTypeIF pointer = baseType;
			for (int i = 0; i < node.getChildCount() - 1; i++) {
				pointer = new ASTPointerType(pointer);
			}
			return this.processDirectDeclarator(
					(CommonTree) (node.getChild(node.getChildCount() - 1)),
					pointer);
		}
	}

	private NameTypePair processDirectDeclarator(CommonTree node,
			ASTTypeIF baseType) throws SyntaxException {
		// For now, we don't allow partially specified array in the program, so
		// codes like a[][2], a[][2][]
		// are illegal. It is either a[][] or a[2][2].
		// a, a[1], a[2][3] ...
		if (node.getChild(0).getType() == MiniMPLexer.IDENTIFIER) {
			ASTIdentifier name = this
					.processID((CommonTree) (node.getChild(0)));
			ASTTypeIF arrayType = baseType;
			boolean hasDimension = false;
			this.dimensionStack = new Stack<ASTExpressionIF>();
			if (node.getChildCount() > 1) {
				for (int i = 1; i < node.getChildCount(); i++) {
					if (i == 1) {
						if (node.getChild(1).getChild(0).getType() == MiniMPLexer.EXPR) {
							hasDimension = true;
						}
					}
					arrayType = this.processDeclaratorSuffix(
							(CommonTree) (node.getChild(i)), arrayType,
							hasDimension);
				}
			}
			if (!this.dimensionStack.empty()) {
				ASTTypeIF headerType = arrayType;
				while (headerType instanceof ASTArrayType) {
					headerType = ((ASTArrayType) headerType).getBaseType();
				}
				while (!this.dimensionStack.empty()) {
					headerType = new ASTArrayType(headerType,
							this.dimensionStack.peek());
					ASTArrayHeader temp = new ASTArrayHeader(headerType,
							this.dimensionStack.pop());
					temp.setElementType(this.arrayHeader);
					this.arrayHeader = temp;
				}
				arrayType = headerType;
			}
			NameTypePair result = new NameTypePair(name, arrayType);
			return result;
		}
		// int (*a)[2] ...
		else {
			ASTTypeIF arrayType = baseType;
			boolean hasDimension = false;
			this.dimensionStack = new Stack<ASTExpressionIF>();
			if (node.getChildCount() > 1) {
				for (int i = 2; i < node.getChildCount(); i++) {
					if (i == 2) {
						if (node.getChild(2).getChild(0).getType() == MiniMPLexer.EXPR) {
							hasDimension = true;
							if (this.arrayHeader != null) {
								this.arrayHeader = null;
							}
						}
					}
					arrayType = this.processDeclaratorSuffix(
							(CommonTree) (node.getChild(i)), arrayType,
							hasDimension);
				}
			}

			if (!this.dimensionStack.empty()) {
				ASTTypeIF headerType = arrayType;
				while (headerType instanceof ASTArrayType) {
					headerType = ((ASTArrayType) headerType).getBaseType();
				}
				while (!this.dimensionStack.empty()) {
					headerType = new ASTArrayType(headerType,
							this.dimensionStack.peek());
					ASTArrayHeader temp = new ASTArrayHeader(headerType,
							this.dimensionStack.pop());
					temp.setElementType(this.arrayHeader);
					this.arrayHeader = temp;
				}
				arrayType = headerType;
			}
			return this.processDeclarator((CommonTree) (node.getChild(0)),
					arrayType);
		}
	}

	private ASTTypeIF processDeclaratorSuffix(CommonTree node,
			ASTTypeIF baseType, boolean hasDimension) throws SyntaxException {
		ASTExpressionIF length = null;
		ASTTypeIF result = null;
		if (node.getChild(0).getType() == MiniMPLexer.EXPR) {
			if (hasDimension == false) {
				this.reportSyntaxException(
						"Partially specified array is not allowed.",
						node.getLine(), node.getCharPositionInLine());
			} else {
				length = this.processExpr((CommonTree) (node.getChild(0)));
				this.dimensionStack.push(length);
				result = new ASTArrayType(baseType);
			}
		} else {
			if (hasDimension) {
				this.reportSyntaxException(
						"Partially specified array is not allowed.",
						node.getLine(), node.getCharPositionInLine());
				/*
				 * } else if (this.isProcessingFunction == false) { // TODO
				 * --this is allowed in some case, such as // initializer with
				 * literal
				 * this.reportSyntaxException("Missing array size information.",
				 * node.getLine(), node.getCharPositionInLine());
				 */
			} else {
				result = new ASTArrayType(baseType);
			}
		}
		return result;
	}

	private ASTExpressionIF processInitializer(CommonTree node,
			ASTTypeIF declType) throws SyntaxException {
		ASTExpressionIF value = null;
		// First handle strings.
		if (node.getChildCount() == 1) {
			value = this.processExpr((CommonTree) (node.getChild(0)));
			if (value instanceof ASTArrayLiteral
					&& ((ASTArrayType) value.getType()).getBaseType() instanceof ASTCharType) {

				return value;
			}
		}
		// simple initialization
		if (node.getChildCount() == 1) {
			// value = this.processExpr((CommonTree) (node
			// .getChild(0)));
			// It's a standalone simple initializer
			if (this.indexList == null) {
				return value;
			}
			// This initializer is in the middle of a complex initializer. It
			// has array/struct index/member information.
			else {
				ASTTypeIF temp = declType;

				for (int i = 0; i < this.indexList.size(); i++) {
					int length;
					if (temp instanceof ASTArrayType) {
						length = Integer
								.valueOf(((ASTIntegerLiteral) (((ASTArrayType) temp)
										.getLength())).getValue());
					} else {
						length = ((ASTStructType) temp).numFieldTypes();
					}
					int index = this.indexList.get(i);
					if (index >= length) {
						this.reportSyntaxException(
								"Array element excess array bounds.",
								node.getLine(), node.getCharPositionInLine());
					}

					if (temp instanceof ASTArrayType) {
						temp = ((ASTArrayType) temp).getBaseType();
					} else if (temp instanceof ASTStructType) {
						temp = ((ASTStructType) temp).getFieldType(index);
					} else {
						this.reportSyntaxException(
								"Too many array indices or too deep struct reference.",
								node.getLine(), node.getCharPositionInLine());
					}

				}
				// Add indices to the index stack
				if (temp instanceof ASTArrayType
						|| temp instanceof ASTStructType) {
					while (temp instanceof ASTArrayType
							|| temp instanceof ASTStructType) {
						this.indexStack.push(new ASTIntegerLiteral(
								new ASTIntegerType(), "0"));
						this.indexList.add(new Integer(0));
						this.designatorCount++;
						if (temp instanceof ASTArrayType) {
							temp = ((ASTArrayType) temp).getBaseType();
						} else {
							temp = ((ASTStructType) temp).getFieldType(0);
						}
					}
				} else {
					if (this.hasProcessedDesignation == false) {
						if (declType instanceof ASTArrayType) {
							this.indexList = this.findNextElement(
									(ASTArrayType) declType, node,
									this.indexList);
						} else if (declType instanceof ASTStructType) {
							this.indexList = this.findNextField(
									(ASTStructType) declType, node,
									this.indexList);
						}
						this.indexStack.clear();
						for (int i = 0; i < this.indexList.size(); i++) {
							this.indexStack.push(new ASTIntegerLiteral(
									new ASTIntegerType(), String
											.valueOf(this.indexList.get(i))));
						}
					}
				}

				Integer[] indexArray = new Integer[this.indexList.size()];
				this.indexList.toArray(indexArray);
				if (declType instanceof ASTArrayType) {
					this.arrayLiteral.setLiteral(indexArray, value);
				} else {
					this.structLiteral.setFieldValue(indexArray, value);
				}
				this.hasProcessedDesignation = false;
				return value;
			}
		}
		// complex initialization such as int a[3] = {1, 2, 3}, will return a
		// literal array expression
		else {
			if (node.getChildCount() == 2) {
				if (declType instanceof ASTArrayType) {
					return new ASTArrayLiteral(declType, new ASTExpressionIF[0]);
				} else {
					return new ASTStructLiteral(declType,
							new ASTExpressionIF[0]);
				}
			} else {
				this.fromInitializer = true;
				this.minDepth++;
				if (this.firstInitList) {
					firstInitList = false;
				} else {
					this.isInDifferentList = true;
				}
				this.processInitializerList((CommonTree) (node.getChild(1)),
						declType);
				this.isInDifferentList = false;
				this.minDepth--;
			}
			return null;
		}
	}

	private void processInitializerList(CommonTree node, ASTTypeIF declType)
			throws SyntaxException {
		ASTTypeIF temp = declType;
		if (this.fromInitializer) {
			while (this.designatorCount > 0) {
				this.indexStack.pop();
				this.indexList.remove(this.indexList.size() - 1);
				this.designatorCount--;
			}
			if (!this.indexStack.empty()) {
				if (this.hasProcessedDesignation == false) {
					int topIndex = this.indexList
							.get(this.indexList.size() - 1) + 1;
					this.indexList.remove(this.indexList.size() - 1);
					this.indexList.add(topIndex);
					this.indexStack.pop();
					this.indexStack.push(new ASTIntegerLiteral(
							new ASTIntegerType(), String.valueOf(topIndex)));
				}
			}
		}

		for (int i = 0; i < node.getChildCount(); i++) {
			if (node.getChild(i).getType() == MiniMPLexer.DESIGNATION) {
				this.processDesignation((CommonTree) (node.getChild(i)), temp);
			} else if (node.getChild(i).getType() == MiniMPLexer.INITIALIZER) {
				this.processInitializer((CommonTree) (node.getChild(i)), temp);
			} else if (node.getChild(i).getType() == MiniMPLexer.INITIALIZER_LIST) {
				this.fromInitializer = false;
				this.processInitializerList((CommonTree) (node.getChild(i)),
						temp);
			} else {
				continue;
			}
		}
	}

	/** Designation is a series of array indices and struct member names */
	private ASTTypeIF processDesignation(CommonTree node, ASTTypeIF declType)
			throws SyntaxException {
		if (this.designatorCount > 0) {
			while (this.designatorCount > 0) {
				this.indexStack.pop();
				this.indexList.remove(this.indexList.size() - 1);
				this.designatorCount--;
			}
		}
		this.hasProcessedDesignation = true;
		return this.processDesignatorList((CommonTree) (node.getChild(0)),
				declType);
	}

	private ASTTypeIF processDesignatorList(CommonTree node, ASTTypeIF declType)
			throws SyntaxException {
		ASTTypeIF result = declType;

		if (this.isInDifferentList == false) {
			if (this.indexList.size() > this.minDepth) {
				while (this.indexList.size() > this.minDepth) {
					this.indexStack.pop();
					this.indexList.remove(this.indexList.size() - 1);
				}
			}
		}

		for (int i = 0; i < node.getChildCount(); i++) {
			ASTExpressionIF designator = this.processDesignator(
					(CommonTree) (node.getChild(i)), declType);

			if (!(designator instanceof ASTLiteralExpression)) {
				this.reportSyntaxException(
						"Constant expression expected in initializer", node
								.getChild(i).getLine(), node.getChild(i)
								.getCharPositionInLine());
			}
			// array index or struct reference
			else if (designator instanceof ASTIntegerLiteral) {
				int index = Integer.valueOf(((ASTIntegerLiteral) designator)
						.getValue());

				if (result instanceof ASTArrayType) {
					int length = Integer
							.valueOf(((ASTIntegerLiteral) (((ASTArrayType) result)
									.getLength())).getValue());
					if (index > length - 1) {
						this.reportSyntaxException(
								"Array index exceeds array bound.", node
										.getChild(i).getLine(), node
										.getChild(i).getCharPositionInLine());
					}
				}
				// Add the index to the stack and list
				this.indexStack.push(designator);
				this.indexList.add(Integer
						.valueOf(((ASTIntegerLiteral) designator).getValue()));
				if (result instanceof ASTArrayType) {
					result = ((ASTArrayType) result).getBaseType();
				} else {
					result = ((ASTStructType) result).getFieldType(Integer
							.valueOf(((ASTIntegerLiteral) designator)
									.getValue()));
				}
			}
			// struct member
			/*
			 * Not implemented yet
			 */
			else {
				this.reportSyntaxException(
						"Struct initializer under development.",
						node.getLine(), node.getCharPositionInLine());
			}
		}
		return result;
	}

	private ASTExpressionIF processDesignator(CommonTree node,
			ASTTypeIF declType) throws SyntaxException {
		ASTExpressionIF result = null;
		// array subscript
		if (node.getChildCount() == 2) {
			result = this
					.processIfThenElseExpr((CommonTree) (node.getChild(0)));
		}
		// struct member reference
		else {
			ASTIdentifier id = this.processID((CommonTree) (node.getChild(0)));
			if (declType instanceof ASTStructType) {
				int index = ((ASTStructType) declType).getFieldIndex(id
						.toString());
				if (index == -1) {
					this.reportSyntaxException(
							"The struct type doesn't contain a field named "
									+ id, node.getLine(),
							node.getCharPositionInLine());
				}
				result = new ASTIntegerLiteral(new ASTIntegerType(),
						String.valueOf(index));
				((ASTIntegerLiteral) result).setFromStructInit(true);
				Source source = this.getSourcePos(node, node);
				result.setSource(source);
				result.setText(this.extractSource(source));
			} else {
				this.reportSyntaxException(
						"Struct type expected for variable declaration with initialization instead of "
								+ declType, node.getLine(),
						node.getCharPositionInLine());
			}
		}
		return result;
	}

	private ASTFunctionDeclaration processFunction(CommonTree node)
			throws SyntaxException {
		ASTTypeIF type = null;
		ASTIdentifier id = null;
		ASTDeclarationIF[] args = null;
		ASTFunction body = null;
		ASTFunctionDeclaration decl = null;
		Source source = null;
		/* If this is a prototype, we do nothing with it */
		if (node.getChild(0).getType() == MiniMPLexer.PROTOTYPE) {
			return null;
		} 
		/* If this is a system function, process appropriately */
		if (node.getChild(0).getType() == MiniMPLexer.SYSTEM) {
			/* Process a guard if one exists */
			if (node.getChild(1).getType() == MiniMPLexer.GUARD) {
				ASTExpressionIF guard = processExpr((CommonTree) (node
						.getChild(2)));
				type = processTypeName((CommonTree) (node.getChild(3)));
				id = processID((CommonTree) (node.getChild(4)));
				this.currentFunction = id;
				this.localVariableMap = new LinkedHashMap<String, ASTDeclarationIF>();
				if (node.getChildCount() == 7) {
					args = processArgumentList((CommonTree) (node.getChild(5)));
				} else {
					args = new ASTDeclarationIF[0];
				}
				decl = new ASTSystemFunctionDeclaration(type, id, args, body,
						guard);
				// Set the source field
				if (node.getChildCount() == 7) {
					source = getSourcePos((CommonTree) (node.getChild(0)),
							(CommonTree) (node.getChild(6)));
					this.lastPosition = new Source(this.file, node.getChild(6)
							.getLine(), node.getChild(6).getLine(), node
							.getChild(6).getCharPositionInLine(), node
							.getChild(6).getCharPositionInLine());
				} else {
					source = getSourcePos((CommonTree) (node.getChild(0)),
							(CommonTree) (node.getChild(5)));
					this.lastPosition = new Source(this.file, node.getChild(5)
							.getLine(), node.getChild(5).getLine(), node
							.getChild(5).getCharPositionInLine(), node
							.getChild(5).getCharPositionInLine());
				}
			} else {
				type = processTypeName((CommonTree) (node.getChild(1)));
				id = processID((CommonTree) (node.getChild(2)));
				this.currentFunction = id;
				this.localVariableMap = new LinkedHashMap<String, ASTDeclarationIF>();
				if (node.getChildCount() == 5) {
					args = processArgumentList((CommonTree) (node.getChild(3)));
				} else {
					args = new ASTDeclarationIF[0];
				}
				decl = new ASTSystemFunctionDeclaration(type, id, args, body,
						null);
				// Set the source field
				if (node.getChildCount() == 5) {
					source = getSourcePos((CommonTree) (node.getChild(0)),
							(CommonTree) (node.getChild(4)));
					this.lastPosition = new Source(this.file, node.getChild(4)
							.getLine(), node.getChild(4).getLine(), node
							.getChild(4).getCharPositionInLine(), node
							.getChild(4).getCharPositionInLine());
				} else {
					source = getSourcePos((CommonTree) (node.getChild(0)),
							(CommonTree) (node.getChild(3)));
					this.lastPosition = new Source(this.file, node.getChild(3)
							.getLine(), node.getChild(3).getLine(), node
							.getChild(3).getCharPositionInLine(), node
							.getChild(3).getCharPositionInLine());
				}
			}
		} else {
			type = processTypeName((CommonTree) (node.getChild(0)));
			id = processID((CommonTree) (node.getChild(1)));

			this.currentFunction = id;
			this.localVariableMap = new LinkedHashMap<String, ASTDeclarationIF>();

			if (node.getChildCount() == 6) {
				args = processArgumentList((CommonTree) (node.getChild(2)));
				body = processFunctionBody((CommonTree) (node.getChild(4)),
						args);
			} else {
				args = new ASTDeclarationIF[0];
				body = processFunctionBody((CommonTree) (node.getChild(3)),
						args);
			}
			// Add a return statement if there is an empty body
			if (body.getStatementList().size() == 0) {
				List<ASTStatementIF> stmtList = new Vector<ASTStatementIF>();
				ASTExpressionIF returnExpression = getGenericExpression(type);
				stmtList.add(new ASTReturnStatement(returnExpression));
				body = new ASTFunction(body.getLocalVariableMap(), stmtList);
			}
			decl = new ASTFunctionDeclaration(type, id, args, body);
			// Set the source field
			if (node.getChildCount() == 6) {
				source = getSourcePos((CommonTree) (node.getChild(0)),
						(CommonTree) (node.getChild(3)));
				this.lastPosition = new Source(this.file, node.getChild(5)
						.getLine(), node.getChild(5).getLine(), node
						.getChild(5).getCharPositionInLine(), node.getChild(5)
						.getCharPositionInLine());
			} else {
				source = getSourcePos((CommonTree) (node.getChild(0)),
						(CommonTree) (node.getChild(2)));
				this.lastPosition = new Source(this.file, node.getChild(4)
						.getLine(), node.getChild(4).getLine(), node
						.getChild(4).getCharPositionInLine(), node.getChild(4)
						.getCharPositionInLine());
			}
		}
		decl.setSource(source);
		decl.setText(extractSource(source));
		this.lastPosition.setText(extractSource(this.lastPosition));
		return decl;
	}

	private ASTExpressionIF getGenericExpression(ASTTypeIF type)
			throws SyntaxException {
		ASTExpressionIF returnExpression = null;
		if (type instanceof ASTArrayType) {
			returnExpression = new ASTArrayLiteral(type, new ASTExpressionIF[0]);
		} else if (type instanceof ASTBoolType) {
			returnExpression = new ASTBoolLiteral(type, true);
		} else if (type instanceof ASTCharType) {
			returnExpression = new ASTCharLiteral(type, 'a');
		} else if (type instanceof ASTIntegerType) {
			returnExpression = new ASTIntegerLiteral(0);
		} else if (type instanceof ASTPointerType) {
			returnExpression = new ASTAddressOfExpression(returnExpression);
		} else if (type instanceof ASTRealType) {
			returnExpression = new ASTRealLiteral(type, "0.0");
		} else if (type instanceof ASTStructType) {
			returnExpression = new ASTStructLiteral(type);
		} else if (type instanceof ASTUnknownType) {
			returnExpression = getGenericExpression(typeNameMap
					.get(((ASTUnknownType) type).getName()));
		}
		return returnExpression;
	}

	private ASTAbstractFunctionDeclaration processAbstractFunction(
			CommonTree node) throws SyntaxException {
		ASTTypeIF type = processTypeName((CommonTree) (node.getChild(2)));
		ASTIdentifier id = processID((CommonTree) (node.getChild(3)));
		CommonTree contNode = (CommonTree) node.getChild(0);

		int continuity = 0;

		if (contNode.getType() != MiniMPLexer.IGNORE)
			continuity = Integer.parseInt(contNode.getText());

		this.localVariableMap = new LinkedHashMap<String, ASTDeclarationIF>();

		ASTDeclarationIF[] args = null;
		// Implementation body = null;
		ASTAbstractFunctionDeclaration decl = null;
		Source source = null;
		if (node.getChildCount() == 6) {
			args = processArgumentList((CommonTree) (node.getChild(4)));
		} else {
			args = new ASTDeclarationIF[0];
		}
		decl = new ASTAbstractFunctionDeclaration(type, id, args, null,
				continuity);
		// Set the source field
		if (node.getChildCount() == 6) {
			source = getSourcePos((CommonTree) (node.getChild(2)),
					(CommonTree) (node.getChild(4)));
		} else {
			source = getSourcePos((CommonTree) (node.getChild(2)),
					(CommonTree) (node.getChild(2)));
		}
		decl.setSource(source);
		decl.setText(extractSource(source));
		return decl;
	}

	private ASTDeclarationIF[] processArgumentList(CommonTree node)
			throws SyntaxException {
		// Because the comma is added in the AST, so the real number of
		// arguments is the
		// number of children plus 1 and divided by 2.
		ASTDeclarationIF[] arguments = new ASTDeclarationIF[(node
				.getChildCount() + 1) / 2];

		ASTDeclarationIF decl = null;

		for (int i = 0; i < node.getChildCount(); i = i + 2) {
			decl = processArgument((CommonTree) (node.getChild(i)), i / 2);
			arguments[i / 2] = decl;
		}
		return arguments;
	}

	private ASTDeclarationIF processArgument(CommonTree node, int index)
			throws SyntaxException {
		ASTTypeIF type = this.processTypeSpecifier((CommonTree) (node
				.getChild(0)));
		NameTypePair pair = this.processDeclarator(
				(CommonTree) (node.getChild(1)), type);
		ASTDeclarationIF result = new ASTFormalParameterDeclaration(
				pair.getName(), pair.getType(), index);
		Source source = null;
		// Set the source field
		source = getSourcePos((CommonTree) (node.getChild(0)),
				(CommonTree) (node.getChild(node.getChildCount() - 1)));
		result.setSource(source);
		result.setText(extractSource(source));
		// Put the formal variables into the local variable map
		this.localVariableMap.put(result.getName().toString(), result);
		this.arrayHeader = null;
		return result;
	}

	private ASTFunction processFunctionBody(CommonTree node,
			ASTDeclarationIF[] argumentList) throws SyntaxException {
		List<ASTStatementIF> stmtList = new Vector<ASTStatementIF>();
		// Has local variables and statements
		if (node.getChildCount() == 2) {
			// Put all the formal parameters in the local variable map
			for (ASTDeclarationIF decl : argumentList) {
				this.localVariableMap.put(decl.getName().toString(), decl);
			}
			this.processDeclarationList((CommonTree) (node.getChild(0)));
			stmtList = processStmtList((CommonTree) (node.getChild(1)));
		}
		// Has local variable or statements
		else if (node.getChildCount() == 1) {
			if (node.getChild(0).getType() == MiniMPLexer.DECL_LIST) {
				// Put all the formal parameters in the local variable map
				for (ASTDeclarationIF decl : argumentList) {
					this.localVariableMap.put(decl.getName().toString(), decl);
				}
				this.processDeclarationList((CommonTree) (node.getChild(0)));
			} else {
				stmtList = processStmtList((CommonTree) (node.getChild(0)));
			}
		}
		// Empty functionbody
		else {
		}
		return new ASTFunction(new LinkedHashMap<String, ASTDeclarationIF>(
				this.localVariableMap), stmtList);
	}

	private List<ASTStatementIF> processStmtList(CommonTree node)
			throws SyntaxException {
		List<ASTStatementIF> stmtList = new Vector<ASTStatementIF>();
		for (int i = 0; i < node.getChildCount(); i++) {
			stmtList.add(processStatement((CommonTree) (node.getChild(i))));
		}
		return stmtList;
	}

	private ASTIdentifier processID(CommonTree node) {
		ASTIdentifier id = new ASTIdentifier(node.getText());
		Source source = getSourcePos(node, node);
		id.setSource(source);
		id.setText(id.toString());
		return id;
	}

	private ASTExpressionIF processExpr(CommonTree node) throws SyntaxException {
		if (node.getChild(0).getType() == MiniMPLexer.ASSIGN_EXPR) {
			// expr: assign_expr
			return processAssignExpr((CommonTree) (node.getChild(0)));
		} else if (node.getChild(0).getType() == MiniMPLexer.IFTHENELSE_EXPR) {
			return processIfThenElseExpr((CommonTree) (node.getChild(0)));
		} else {
			// expr: quantifier_expr
			return processQuantifierExpr((CommonTree) (node.getChild(0)));
		}
	}

	private ASTExpressionIF processAssignExpr(CommonTree node)
			throws SyntaxException {
		if (node.getChildCount() == 3) {
			ASTExpressionIF lhsTemp = processUnaryExpr((CommonTree) (node
					.getChild(0)));
			if (!(lhsTemp instanceof ASTLhsExpressionIF)) {
				this.reportSyntaxException(
						"Left value expected in assignment.", node.getChild(0)
								.getLine(), node.getChild(0)
								.getCharPositionInLine());
			}
			ASTLhsExpressionIF lhs = (ASTLhsExpressionIF) lhsTemp;

			ASTExpressionIF temp = processAssignExpr((CommonTree) (node
					.getChild(2)));
			ASTExpressionIF rhs = null;

			switch (node.getChild(1).getType()) {
			case MiniMPLexer.ASSIGN:
				rhs = temp;
				break;
			case MiniMPLexer.PLUS_ASSIGN:
				rhs = new ASTBinaryExpression(BinaryOperator.PLUS, lhs, temp);
				break;
			case MiniMPLexer.SUB_ASSIGN:
				rhs = new ASTBinaryExpression(BinaryOperator.SUB, lhs, temp);
				break;
			case MiniMPLexer.MULTI_ASSIGN:
				rhs = new ASTBinaryExpression(BinaryOperator.MUL, lhs, temp);
				break;
			case MiniMPLexer.DIV_ASSIGN:
				rhs = new ASTBinaryExpression(BinaryOperator.DIV, lhs, temp);
				break;
			case MiniMPLexer.MOD_ASSIGN:
				rhs = new ASTBinaryExpression(BinaryOperator.MOD, lhs, temp);
				break;
			default:
				throw new edu.udel.cis.vsl.tass.model.IF.SyntaxException(
						temp.getSource(), "Unknown operator type "
								+ node.getChild(1).getText() + " : "
								+ node.getLine());
			}

			ASTExpressionIF result = new ASTAssignExpression(lhs, rhs);
			Source source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			result.setSource(source);
			String text = extractSource(source);
			if (text.endsWith(";") || text.endsWith(")")) {
				text = text.substring(0, text.length() - 1);
			}
			result.setText(text);
			return result;
		} else {
			return processIfThenElseExpr((CommonTree) (node.getChild(0)));
		}
	}

	private ASTExpressionIF processIfThenElseExpr(CommonTree node)
			throws SyntaxException {
		if (node.getChildCount() == 1) {
			return processLogicalOrExpr((CommonTree) (node.getChild(0)));
		} else {
			ASTExpressionIF predicate = processLogicalOrExpr((CommonTree) (node
					.getChild(0)));
			ASTExpressionIF trueExpr = processExpr((CommonTree) (node
					.getChild(1)));
			ASTExpressionIF falseExpr = processExpr((CommonTree) (node
					.getChild(2)));
			ASTExpressionIF result = new ASTIfThenElseExpression(predicate,
					trueExpr, falseExpr);
			Source source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			result.setSource(source);
			result.setText(extractSource(source));
			return result;
		}
	}

	private ASTExpressionIF processQuantifierExpr(CommonTree node)
			throws SyntaxException {
		if (node.getChildCount() == 1) {
			return processLogicalOrExpr((CommonTree) (node.getChild(0)));
		} else {
			if (node.getChild(0).getChild(0).getType() == MiniMPLexer.FORALL) {
				return processQuantifierExpr(node,
						ASTQuantifierExpression.QuantifierKind.FORALL);
			} else if (node.getChild(0).getChild(0).getType() == MiniMPLexer.EXISTS) {
				return processQuantifierExpr(node,
						ASTQuantifierExpression.QuantifierKind.EXISTS);
			}

			reportSyntaxException("Unexpected quantifier type", node.getLine(),
					0);
			return null;
		}
	}

	private ASTExpressionIF processQuantifierExpr(CommonTree node,
			QuantifierKind quantifierType) throws SyntaxException {
		ASTTypeIF type = processSimpleType((CommonTree) node.getChild(1));
		ASTIdentifier identifier = processID((CommonTree) node.getChild(2));

		ASTDeclarationIF declaration = new ASTSimpleVariableDeclaration(
				identifier, type, VariableCategory.BOUND);
		declaration.setSource(getSourcePos((CommonTree) node.getChild(1),
				(CommonTree) node.getChild(3)));
		// Initialize the map if it hasn't been already
		if (this.boundVariableMap == null)
			this.boundVariableMap = new LinkedHashMap<String, ASTDeclarationIF>();
		// Create a temporary storage place in case a bound variable of the same
		// name
		// existed at a higher scope
		ASTDeclarationIF oldDeclaration = this.boundVariableMap.get(declaration
				.getName().toString());
		boundVariableMap.put(declaration.getName().toString(), declaration);
		ASTExpressionIF boundExpression = null;
		int expressionIndex = 3;
		if (node.getChild(3).getType() == MiniMPLexer.BAR) {
			boundExpression = processLogicalOrExpr((CommonTree) node
					.getChild(4));
			expressionIndex = 5;
		}

		ASTExpressionIF expression = processExpr((CommonTree) node
				.getChild(expressionIndex));
		ASTExpressionIF identifierExpression = new ASTVariableExpression(
				identifier, type);

		identifierExpression.setSource(identifier.source());
		identifierExpression.setText(identifier.toString());
		ASTQuantifierExpression result = new ASTQuantifierExpression(
				quantifierType, identifierExpression, boundExpression,
				expression);
		Source source = getSourcePos((CommonTree) (node.getChild(0)),
				(CommonTree) (node.getChild(node.getChildCount() - 1)));
		result.setSource(source);
		result.setText(extractSource(source));
		// Restore variable from a higher scope, if necessary
		if (oldDeclaration != null)
			boundVariableMap.put(declaration.getName().toString(),
					oldDeclaration);
		else
			boundVariableMap.remove(declaration.getName().toString());
		return result;
	}

	private ASTExpressionIF processLogicalOrExpr(CommonTree node)
			throws SyntaxException {
		Source source = null;
		ASTExpressionIF expr = null;

		// logical_or_expr: logical_and_expr
		if (node.getChildCount() == 1) {
			return processLogicalAndExpr((CommonTree) (node.getChild(0)));
		}
		// logical_or_expr: logical_and_expr (|| logical_and_expr)*
		else {
			ASTExpressionIF left = null;

			for (int i = 0; i < node.getChildCount() - 2; i += 2) {
				if (i == 0) {
					left = processLogicalAndExpr((CommonTree) (node.getChild(i)));
				} else {
					left = expr;
				}
				expr = new ASTBinaryExpression(BinaryOperator.OR, left,
						processLogicalAndExpr((CommonTree) (node
								.getChild(i + 2))));
			}
			// Set the source field
			source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			expr.setSource(source);
			expr.setText(extractSource(source));
			return expr;
		}
	}

	private ASTExpressionIF processLogicalAndExpr(CommonTree node)
			throws SyntaxException {
		Source source = null;
		ASTExpressionIF expr = null;
		// logical_and_expr: equality_expr
		if (node.getChildCount() == 1) {
			return processEqualityExpr((CommonTree) (node.getChild(0)));
		}
		// logical_and_expr: equality_expr (&& equality_expr)*
		else {

			ASTExpressionIF left = null;
			for (int i = 0; i < node.getChildCount() - 2; i += 2) {
				if (i == 0) {
					left = processEqualityExpr((CommonTree) (node.getChild(i)));
				} else {
					left = expr;
				}
				expr = new ASTBinaryExpression(
						BinaryOperator.AND,
						left,
						processEqualityExpr((CommonTree) (node.getChild(i + 2))));
			}
			// Set the source field
			source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			expr.setSource(source);
			expr.setText(extractSource(source));
			return expr;
		}
	}

	private ASTExpressionIF processEqualityExpr(CommonTree node)
			throws SyntaxException {
		Source source = null;
		ASTExpressionIF expr = null;
		// equality_expr: relational_expr
		if (node.getChildCount() == 1) {
			return processRelationalExpr((CommonTree) (node.getChild(0)));
		}
		// equality: relational_expr (== relational_expr | != relational_expr)*
		else {
			ASTExpressionIF left = null;
			String op = null;
			BinaryOperator operator = null;

			for (int i = 0; i < node.getChildCount() - 2; i += 2) {
				// process the operator
				op = node.getChild(i + 1).getText();

				if (op.equalsIgnoreCase("==")) {
					operator = BinaryOperator.EQ;
				} else if (op.equalsIgnoreCase("!=")) {
					operator = BinaryOperator.NEQ;
				} else {
					this.reportSyntaxException("Unknown operator type: " + op,
							node.getChild(i + 1).getLine(), node
									.getChild(i + 1).getCharPositionInLine());
				}

				// assemble the expression
				if (i == 0) {
					left = processRelationalExpr((CommonTree) (node.getChild(0)));
				} else {
					left = expr;
				}

				expr = new ASTBinaryExpression(operator, left,
						processRelationalExpr((CommonTree) (node
								.getChild(i + 2))));
			}

			// Set the source field
			source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			expr.setSource(source);
			expr.setText(extractSource(source));
			return expr;
		}
	}

	private ASTExpressionIF processRelationalExpr(CommonTree node)
			throws SyntaxException {
		Source source = null;
		ASTExpressionIF expr = null;
		if (node.getChildCount() == 1) {
			return processAdditiveExpr((CommonTree) (node.getChild(0)));
		} else {
			String op = null;
			ASTExpressionIF left = null;

			BinaryOperator operator = null;
			for (int i = 0; i < node.getChildCount() - 2; i += 2) {
				// process the operator
				op = node.getChild(i + 1).getText();
				if (op.equalsIgnoreCase("<")) {
					operator = BinaryOperator.LT;
				} else if (op.equalsIgnoreCase("<=")) {
					operator = BinaryOperator.LTE;
				} else if (op.equalsIgnoreCase(">")) {
					operator = BinaryOperator.GT;
				} else if (op.equalsIgnoreCase(">=")) {
					operator = BinaryOperator.GTE;
				} else {
					this.reportSyntaxException("Unknow operator type: " + op,
							node.getChild(i + 1).getLine(), node
									.getChild(i + 1).getCharPositionInLine());
				}
				// assemble the expression
				if (i == 0) {
					left = processAdditiveExpr((CommonTree) (node.getChild(0)));
				} else {
					left = expr;
				}
				ASTExpressionIF right = processAdditiveExpr((CommonTree) (node
						.getChild(i + 2)));
				if (i + 2 == node.getChildCount() - 1) {
					lastLine = right.getSource().lastLine();
					lastColumn = right.getSource().lastColumn();
				}
				expr = new ASTBinaryExpression(operator, left, right);
			}
			// Set the source field
			source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			expr.setSource(source);
			expr.setText(extractSource(source));
			return expr;
		}
	}

	// + and -
	private ASTExpressionIF processAdditiveExpr(CommonTree node)
			throws SyntaxException {
		Source source = null;
		ASTExpressionIF expr = null;
		if (node.getChildCount() == 1) {
			return processMultiplicativeExpr((CommonTree) (node.getChild(0)));
		} else {
			String op = null;
			BinaryOperator operator = null;
			ASTExpressionIF left = null;
			for (int i = 0; i < node.getChildCount() - 2; i += 2) {
				// process the operator
				op = node.getChild(i + 1).getText();

				if (op.equalsIgnoreCase("+")) {
					operator = BinaryOperator.PLUS;
				} else if (op.equalsIgnoreCase("-")) {
					operator = BinaryOperator.SUB;
				} else {
					this.reportSyntaxException("Unknown operator type: " + op,
							node.getChild(i + 1).getLine(), node
									.getChild(i + 1).getCharPositionInLine());
				}

				// assemble the expression
				if (i == 0) {
					left = processMultiplicativeExpr((CommonTree) (node
							.getChild(i)));
				} else {
					left = expr;
				}
				expr = new ASTBinaryExpression(operator, left,
						processMultiplicativeExpr((CommonTree) (node
								.getChild(i + 2))));
			}

			// Set the source field
			source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			expr.setSource(source);
			expr.setText(extractSource(source));
			return expr;
		}
	}

	private ASTExpressionIF processMultiplicativeExpr(CommonTree node)
			throws SyntaxException {
		Source source = null;
		ASTExpressionIF expr = null;
		if (node.getChildCount() == 1) {
			return processUnaryExpr((CommonTree) (node.getChild(0)));
		} else {
			String op = null;
			BinaryOperator operator = null;
			ASTExpressionIF left = null;

			for (int i = 0; i < node.getChildCount() - 2; i += 2) {
				// process the oeprator
				op = node.getChild(i + 1).getText();

				if (op.equalsIgnoreCase("*")) {
					operator = BinaryOperator.MUL;
				} else if (op.equalsIgnoreCase("/")) {
					operator = BinaryOperator.DIV;
				} else if (op.equalsIgnoreCase("%")) {
					operator = BinaryOperator.MOD;
				} else {
					this.reportSyntaxException("Unknow operator type: " + op,
							node.getChild(i + 1).getLine(), node
									.getChild(i + 1).getCharPositionInLine());
				}

				// assemble the expression
				if (i == 0) {
					left = processUnaryExpr((CommonTree) (node.getChild(i)));
				} else {
					left = expr;
				}

				expr = new ASTBinaryExpression(operator, left,
						processUnaryExpr((CommonTree) (node.getChild(i + 2))));
			}
			// Set the source field
			source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			expr.setSource(source);
			expr.setText(extractSource(source));
			return expr;
		}
	}

	private ASTExpressionIF processUnaryExpr(CommonTree node)
			throws SyntaxException {
		Source source = null;
		ASTExpressionIF expr = null;
		// unary_expr -> postfix_expr
		if (node.getChildCount() == 1) {
			return processPostfixExpr((CommonTree) (node.getChild(0)));
		} else {
			// sizeof (type) | sizeof name
			if (node.getChild(0).getType() == MiniMPLexer.SIZEOF) {
				ASTTypeIF operand = null;
				// sizeof int
				if (node.getChild(1).getType() == MiniMPLexer.TYPE_NAME) {
					operand = this.processTypeName((CommonTree) (node
							.getChild(1)));
				}
				// sizeof(a)
				else {
					operand = this.processUnaryExpr(
							(CommonTree) (node.getChild(1))).getType();
				}
				expr = new ASTSizeofExpression(operand);
			} else if (node.getChild(0).getType() == MiniMPLexer.CAST) {
				ASTTypeIF castType = processTypeName((CommonTree) node.getChild(1));
				expr = new ASTTypeCast(
						processUnaryExpr((CommonTree) node.getChild(2)),
						castType);
				
			}
			// (+ | - | & | ! | *) unary_expr
			else if (node.getChild(0).getType() == MiniMPLexer.UNARY_OP) {
				String op = node.getChild(0).getChild(0).getText();
				if (op.equalsIgnoreCase("+")) {
					expr = new ASTUnaryExpression(UnaryOperator.PLUS,
							processUnaryExpr((CommonTree) (node.getChild(1))));
				} else if (op.equalsIgnoreCase("-")) {
					expr = new ASTUnaryExpression(UnaryOperator.MINUS,
							processUnaryExpr((CommonTree) (node.getChild(1))));
				} else if (op.equalsIgnoreCase("~")) {
					expr = new ASTUnaryExpression(UnaryOperator.NOT,
							processUnaryExpr((CommonTree) (node.getChild(1))));
				} else if (op.equalsIgnoreCase("*")) {
					expr = new ASTDereferenceExpression(
							processUnaryExpr((CommonTree) (node.getChild(1))));
				} else if (op.equalsIgnoreCase("&")) {
					expr = new ASTAddressOfExpression(
							processUnaryExpr((CommonTree) (node.getChild(1))));
				} else {
					this.reportSyntaxException("Unknow operator type: " + op,
							node.getChild(0).getLine(), node.getChild(0)
									.getCharPositionInLine());
				}
			}
			// (++ | --) unary_expr
			else {
				String op = node.getChild(0).getChild(0).getText();
				ASTExpressionIF body = this.processUnaryExpr((CommonTree) (node
						.getChild(1)));
				if (!(body instanceof ASTLhsExpressionIF)) {
					this.reportSyntaxException(
							"Left value expected in increment/decrement expressions.",
							node.getChild(1).getLine(), node.getChild(1)
									.getCharPositionInLine());
				}
				if (op.equals("++")) {
					expr = new ASTSelfChangeExpression(
							SelfChangeOperator.INCREMENT,
							(ASTLhsExpressionIF) body, false);
				} else {
					expr = new ASTSelfChangeExpression(
							SelfChangeOperator.DECREMENT,
							(ASTLhsExpressionIF) body, false);
				}
			}
			// Set the source field
			source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			expr.setSource(source);
			expr.setText(extractSource(source));
			return expr;
		}
	}

	private ASTExpressionIF processPostfixExpr(CommonTree node)
			throws SyntaxException {
		ASTExpressionIF result = null;
		Source source = null;
		if (node.getChildCount() == 1) {
			return processPrimaryExpr((CommonTree) (node.getChild(0)));
		} else {
			ASTExpressionIF body = processPrimaryExpr((CommonTree) (node
					.getChild(0)));
			result = this.processPostfixExprSuffix(
					(CommonTree) (node.getChild(1)), body);
			source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			result.setSource(source);
			result.setText(this.extractSource(source));
			return result;
		}
	}

	private ASTExpressionIF processPostfixExprSuffix(CommonTree node,
			ASTExpressionIF body) throws SyntaxException {
		ASTExpressionIF result = null;
		int type = node.getChild(0).getType();
		// struct member reference
		if (type == MiniMPLexer.DOT) {
			ASTExpressionIF temp = null;
			String fieldName = this.processID((CommonTree) (node.getChild(1)))
					.toString();
			ASTTypeIF fieldType = ((ASTStructType) (body.getType()))
					.getFieldType(fieldName);
			if (fieldType instanceof ASTScalarType
					|| fieldType instanceof ASTPointerType) {
				temp = new ASTLhsStructMemberRefExpression(body, fieldName);

			} else {
				temp = new ASTStructMemberRefExpression(body, fieldName);
			}

			// have follow-up constructs
			if (node.getChildCount() == 3) {
				result = this.processPostfixExprSuffix(
						(CommonTree) (node.getChild(2)), temp);
			} else {
				result = temp;
			}
		}
		// function referenced in PROC expression
		else if (type == MiniMPLexer.AT) {
			ASTExpressionIF temp = null;
			String functionName = this.processID(
					(CommonTree) (node.getChild(1))).toString();
			String fieldName = this.processID((CommonTree) (node.getChild(3)))
					.toString();
			fieldName += "@" + functionName;
			ASTTypeIF fieldType = ((ASTStructType) (body.getType()))
					.getFieldType(fieldName);
			if (fieldType instanceof ASTScalarType
					|| fieldType instanceof ASTPointerType) {
				temp = new ASTLhsStructMemberRefExpression(body, fieldName);

			} else {
				temp = new ASTStructMemberRefExpression(body, fieldName);
			}

			// have follow-up constructs
			if (node.getChildCount() == 5) {
				result = this.processPostfixExprSuffix(
						(CommonTree) (node.getChild(4)), temp);
			} else {
				result = temp;
			}
		}
		// struct member reference by pointer
		else if (type == MiniMPLexer.ARROW) {
			ASTTypeIF baseType = null;
			if (!(body.getType() instanceof ASTPointerType)) {
				this.reportSyntaxException(
						"Type error. Expected a pointer type but got "
								+ body.getType(), node.getLine(),
						node.getCharPositionInLine());
			} else {
				baseType = ((ASTPointerType) (body.getType())).getBaseType();
				if (!(baseType instanceof ASTStructType)) {
					this.reportSyntaxException(
							"Type error. Expected a struct type as the base type of the pointer type, but got "
									+ baseType, node.getLine(),
							node.getCharPositionInLine());
				}
			}

			ASTExpressionIF temp = null;
			String fieldName = this.processID((CommonTree) (node.getChild(1)))
					.toString();
			if (!(((ASTStructType) baseType).hasField(fieldName))) {
				this.reportSyntaxException("Struct type " + body.getType()
						+ " doesn't have a field named " + fieldName, node
						.getChild(1).getLine(), node.getChild(1)
						.getCharPositionInLine());
			} else {
				ASTTypeIF fieldType = ((ASTStructType) baseType)
						.getFieldType(fieldName);
				if (fieldType instanceof ASTScalarType
						|| fieldType instanceof ASTPointerType) {
					temp = new ASTLhsStructMemberRefExpression(body, fieldName);
				} else {
					temp = new ASTStructMemberRefExpression(body, fieldName);
				}
			}

			// have follow-up constructs
			if (node.getChildCount() == 3) {
				result = this.processPostfixExprSuffix(
						(CommonTree) (node.getChild(2)), temp);
			} else {
				result = temp;
			}
		}
		// array subscript or pointer dereference
		else if (type == MiniMPLexer.EXPR) {
			if (!(body.getType() instanceof ASTArrayType)
					&& !(body.getType() instanceof ASTPointerType)) {
				this.reportSyntaxException(
						"Type error. Array or pointer type expected in array subscript expression but got "
								+ body.getType().getClass().getSimpleName(),
						node.getLine(), node.getCharPositionInLine());
			}
			ASTExpressionIF index = this.processExpr((CommonTree) (node
					.getChild(0)));
			if (!(index.getType() instanceof ASTIntegerType)) {
				this.reportSyntaxException(
						"Type error. Integer type expected in array index, but got "
								+ index.getType(), node.getLine(),
						node.getCharPositionInLine());
			}
			ASTTypeIF baseType = null;
			if (body.getType() instanceof ASTArrayType) {
				baseType = ((ASTArrayType) (body.getType())).getBaseType();
				if (baseType instanceof ASTScalarType
						|| baseType instanceof ASTPointerType) {
					result = new ASTLhsArraySubscriptExpression(body, index);
				} else {
					result = new ASTArraySubscriptExpression(body, index);
				}
			}
			// p[i] = *(p + i)
			else {
				baseType = ((ASTPointerType) (body.getType())).getBaseType();
				ASTExpressionIF temp = new ASTBinaryExpression(
						BinaryOperator.PLUS, body, index);
				result = new ASTDereferenceExpression(temp);
			}
			// have follow-up constructs
			if (node.getChildCount() == 3) {
				result = this.processPostfixExprSuffix(
						(CommonTree) (node.getChild(2)), result);
			}
		} else if (type == MiniMPLexer.SELFCHANGE_OP) {
			int opType = node.getChild(0).getChild(0).getType();

			if (!(body instanceof ASTLhsExpressionIF)) {
				this.reportSyntaxException(
						"Left value expected in increment/decrement expression, but got "
								+ body.getClass().getSimpleName(),
						node.getLine(), node.getCharPositionInLine());
			}
			if (opType == MiniMPLexer.DOUBLE_PLUS) {
				result = new ASTSelfChangeExpression(
						SelfChangeOperator.INCREMENT,
						(ASTLhsExpressionIF) body, true);
			} else {
				result = new ASTSelfChangeExpression(
						SelfChangeOperator.DECREMENT,
						(ASTLhsExpressionIF) body, true);
			}

			// have follow-up constructs
			if (node.getChildCount() == 2) {
				result = this.processPostfixExprSuffix(
						(CommonTree) (node.getChild(1)), result);
			}
		}
		Source source = getSourcePos((CommonTree) (node.getChild(0)),
				(CommonTree) (node.getChild(node.getChildCount() - 1)));
		result.setSource(source);
		result.setText(this.extractSource(source));
		return result;
	}

	private ASTExpressionIF processSpecExpr(CommonTree node)
			throws SyntaxException {
		ASTIdentifier id = processID((CommonTree) (node.getChild(0)));
		ASTIdentifier function = this.specFunction != null ? this.specFunction
				: this.currentFunction;
		ASTTypeIF specType = null;
		if (this.specProgram == null) {
			this.reportSyntaxException("No spec program.", node.getLine(),
					node.getCharPositionInLine());
		}
		if ((this.specProgram.hasVariable(function, id) == false)
				&& (!id.toString().equals("PROC"))) {
			this.reportSyntaxException("No variable named " + id.toString()
					+ " found in function " + function.toString()
					+ " in the other program.", node.getLine(),
					node.getCharPositionInLine());
		} else if (id.toString().equals("PROC")) {
			if (this.specProgram.getGlobalVariableMap().containsKey("PROC")) {
				specType = this.specProgram.getGlobalVariableMap().get("PROC")
						.getType();
			} else {
				this.reportSyntaxException(
						"The spec program does not contain a reference to process variables",
						node.getLine(), node.getCharPositionInLine());
			}
		} else {
			specType = this.specProgram.getVariable(function, id).getType();
		}
		ASTExpressionIF expr = new ASTSpecExpression(id, specType);
		Source source = getSourcePos((CommonTree) (node.getChild(0)),
				(CommonTree) (node.getChild(node.getChildCount() - 1)));
		expr.setSource(source);
		expr.setText(extractSource(source));
		return expr;
	}

	private ASTExpressionIF processPrimaryExpr(CommonTree node)
			throws SyntaxException {
		ASTExpressionIF result = null;
		// identifier or constant
		if (node.getChildCount() == 1) {
			if (node.getChild(0).getType() == MiniMPLexer.IDENTIFIER) {
				ASTIdentifier name = this.processID((CommonTree) (node
						.getChild(0)));
				ASTDeclarationIF decl = null;
				if (isProcessingSpecVar) {
					// TODO: figure out why specProgram is null during a
					// comparison
					if (specProgram.getGlobalVariableMap().containsKey(
							name.toString())) {
						decl = specProgram.getGlobalVariableMap().get(
								name.toString());
						this.isProcessingSpecVar = false;
					} else {
						this.reportSyntaxException(
								"Undefined variable " + name, node.getLine(),
								node.getCharPositionInLine());
					}
				} else if (this.boundVariableMap != null
						&& this.boundVariableMap.containsKey(name.toString())) {
					decl = this.boundVariableMap.get(name.toString());
				} else if (this.localVariableMap != null
						&& this.localVariableMap.containsKey(name.toString())) {
					decl = this.localVariableMap.get(name.toString());
				} else if (this.globalVariableMap.containsKey(name.toString())) {
					decl = this.globalVariableMap.get(name.toString());
				} else if (this.constantMap.containsKey(name.toString())) {
					return this.constantMap.get(name.toString());
				} else {
					this.reportSyntaxException("Undefined variable " + name,
							node.getLine(), node.getCharPositionInLine());
				}
				if (decl.getType() instanceof ASTScalarType
						|| decl.getType() instanceof ASTPointerType) {
					result = new ASTLhsVariableExpression(name, decl.getType());
				} else {
					result = new ASTVariableExpression(name, decl.getType());
				}
				Source source = getSourcePos((CommonTree) (node.getChild(0)),
						(CommonTree) (node.getChild(node.getChildCount() - 1)));
				result.setSource(source);
				result.setText(this.extractSource(source));
				return result;
			} else if (node.getChild(0).getType() == MiniMPLexer.CONSTANT) {
				return processLiteralExpr((CommonTree) (node.getChild(0)));
			} else if (node.getChild(0).getType() == MiniMPLexer.EVALUATED_FUNCTION_EXPR) {
				return this.processEvaluatedFunctionExpr((CommonTree) (node
						.getChild(0)));
			} else if (node.getChild(0).getType() == MiniMPLexer.DERIVATIVE_EXPR) {
				return this.processDerivativeExpr((CommonTree) (node
						.getChild(0)));
			} else {
				return this.processSpecExpr((CommonTree) (node.getChild(0)));
			}
		}
		// expression wrapped in parenthesis
		else {
			return processExpr((CommonTree) (node.getChild(0)));
		}
	}

	private ASTExpressionIF processDerivativeExpr(CommonTree node)
			throws SyntaxException {
		List<ASTExpressionIF> paramList = new Vector<ASTExpressionIF>();
		ASTIdentifier baseFunctionName = processID((CommonTree) (node
				.getChild(0)));
		String name = null;
		String partialNames = "";
		ASTDeclarationIF decl = null, newDecl = null;
		ASTExpressionIF expr = null;
		ASTTypeIF type = null;

		if (this.localVariableMap != null
				&& this.localVariableMap.containsKey(baseFunctionName
						.toString())) {
			decl = this.localVariableMap.get(baseFunctionName.toString());
		} else if (this.globalVariableMap.containsKey(baseFunctionName
				.toString())) {
			decl = this.globalVariableMap.get(baseFunctionName.toString());
		} else {
			this.reportSyntaxException("Undefined base function "
					+ baseFunctionName, node.getLine(),
					node.getCharPositionInLine());
		}

		type = decl.getType();
		partialNames = processPartialList((CommonTree) (node.getChild(1)));
		if (node.getChildCount() == 4) {
			paramList = processParamList((CommonTree) (node.getChild(2)));
		}
		name = "\\D[" + baseFunctionName.toString() + "," + partialNames + "]";
		newDecl = new ASTAbstractFunctionDeclaration(type, new ASTIdentifier(
				name), ((ASTAbstractFunctionDeclaration) decl).getFormalList(),
				null, ((ASTAbstractFunctionDeclaration) decl).continuity());
		abstractFunctionList.add((ASTAbstractFunctionDeclaration) newDecl);
		expr = new ASTEvaluatedFunction(type, name, paramList);
		return expr;
		// TODO Auto-generated method stub
	}

	private String processPartialList(CommonTree node) {
		String partials = "";
		CommonTree child;
		for (int i = 0; i < node.getChildCount(); i++) {
			if (i != 0) {
				partials += ",";
			}
			child = (CommonTree) node.getChild(i);
			partials += "{" + child.getChild(0).toString() + ","
					+ child.getChild(1).toString() + "}";
		}
		return partials;
	}

	private ASTExpressionIF processEvaluatedFunctionExpr(CommonTree node)
			throws SyntaxException {
		List<ASTExpressionIF> paramList = new Vector<ASTExpressionIF>();
		ASTIdentifier name = processID((CommonTree) (node.getChild(0)));
		ASTDeclarationIF decl = null;
		ASTExpressionIF expr = null;
		ASTTypeIF type = null;

		if (this.localVariableMap != null
				&& this.localVariableMap.containsKey(name.toString())) {
			decl = this.localVariableMap.get(name.toString());
		} else if (this.globalVariableMap.containsKey(name.toString())) {
			decl = this.globalVariableMap.get(name.toString());
		} else {
			this.reportSyntaxException("Undefined variable " + name,
					node.getLine(), node.getCharPositionInLine());
		}
		type = decl.getType();
		if (node.getChildCount() == 3) {
			paramList = processParamList((CommonTree) (node.getChild(1)));
		}
		expr = new ASTEvaluatedFunction(type, name.toString(), paramList);
		return expr;
	}

	private ASTExpressionIF processLiteralExpr(CommonTree node)
			throws SyntaxException {
		ASTExpressionIF expr = null;
		String text;
		
		switch (node.getChild(0).getType()) {
		case MiniMPLexer.TRUE:
			expr = new ASTBoolLiteral(new ASTBoolType(), true);
			break;
		case MiniMPLexer.FALSE:
			expr = new ASTBoolLiteral(new ASTBoolType(), false);
			break;
		case MiniMPLexer.INT_LITERAL:
			text = node.getChild(0).getText();
			text = text.replaceAll("u", "");
			text = text.replaceAll("U", "");
			text = text.replaceAll("l", "");
			text = text.replaceAll("L", "");
			expr = new ASTIntegerLiteral(new ASTIntegerType(), text);
			break;
		case MiniMPLexer.REAL_LITERAL:
			text = node.getChild(0).getText();
			text = text.replaceAll("F", "");
			text = text.replaceAll("f", "");
			expr = new ASTRealLiteral(new ASTRealType(), text);
			break;
		case MiniMPLexer.CHAR_LITERAL:
			char[] charValue = node.getChild(0).getText().toCharArray();
			if (charValue.length - 2 > 1) {
				this.reportSyntaxException(
						"Char value have length greater than 1.",
						node.getLine(), node.getCharPositionInLine());
			}
			char value = charValue[1];
			expr = new ASTCharLiteral(new ASTCharType(), value);
			break;
		case MiniMPLexer.STRING_LITERAL:
			String string = node.getChild(0).getText();
			char[] charArray = string.toCharArray();
			// subtract 2 to get rid of leading and trailing "
			int numChars = charArray.length - 2;
			ASTExpressionIF[] charLiterals = new ASTExpressionIF[numChars];
			ASTTypeIF charType = new ASTCharType();
			ASTIntegerLiteral extent = new ASTIntegerLiteral(numChars);
			ASTArrayType arrayType = new ASTArrayType(charType, extent);

			for (int i = 0; i < numChars; i++) {
				charLiterals[i] = new ASTCharLiteral(charType, charArray[i + 1]);
			}
			expr = new ASTArrayLiteral(arrayType, charLiterals);
			break;
		case MiniMPLexer.SYS_VAR:
			if (node.getChild(0).getText().equals("PID")) {
				expr = new ASTSystemVariable(new ASTIntegerType(), SYS_VAR.PID);
			} else {
				expr = new ASTSystemVariable(new ASTIntegerType(),
						SYS_VAR.NPROCS);
			}
			break;
		default:
			this.reportSyntaxException(
					"Unknown constant type: " + node.getChild(0), node
							.getChild(0).getLine(), node.getChild(0)
							.getCharPositionInLine());
		}
		// Set the source field
		Source source = getSourcePos((CommonTree) (node.getChild(0)),
				(CommonTree) (node.getChild(node.getChildCount() - 1)));
		expr.setSource(source);
		expr.setText(node.getChild(0).getText());
		return expr;
	}

	private ASTStatementIF processStatement(CommonTree node)
			throws SyntaxException {
		CommonTree child = (CommonTree) (node.getChild(0));
		switch (child.getType()) {
		case MiniMPLexer.ASSERT_STMT:
			return processAssertStmt(child);
			/*
			 * case MiniMPLexer.ASSIGNMENT_STMT: return
			 * processAssignmentStmt(child);
			 */
		case MiniMPLexer.ASSUME_STMT:
			return processAssumeStmt(child);
		case MiniMPLexer.CALL_STMT:
			return processCallStmt(child);
		case MiniMPLexer.COMPOUND_STMT:
			return processCompoundStmt(child);
		case MiniMPLexer.CONDITION_STMT:
			return processConditionStmt(child);
		case MiniMPLexer.EMPTY_STMT:
			return processEmptyStmt(child);
		case MiniMPLexer.ITERATIVE_STMT:
			return processIterativeStmt(child);
		case MiniMPLexer.RECV_STMT:
			return processRecvStmt(child);
		case MiniMPLexer.RETURN_STMT:
			return processReturnStmt(child);
		case MiniMPLexer.SELECT_STMT:
			return processSelectStmt(child);
		case MiniMPLexer.SEND_STMT:
			return processSendStmt(child);
		case MiniMPLexer.EXPR_STMT:
			return processExprStmt(child);
		case MiniMPLexer.ALLOCATE_STMT:
			return processAllocateStmt(child);
		case MiniMPLexer.COLLECTIVE_ASSERT_STMT:
			// Ignore collective assertions when doing a comparison
			if (configuration instanceof CompareConfiguration) {
				return new ASTEmptyStatement();
			}
			return processCollectiveAssertStmt(child);
		case MiniMPLexer.JOINT_ASSERT_STMT:
			return processJointAssertStmt(child);
		case MiniMPLexer.INVARIANT_STMT:
			return processInvariantStmt(child);
		case MiniMPLexer.COLLECTIVE_INVARIANT_STMT:
			return processCollectiveInvariantStmt(child);
		case MiniMPLexer.JOINT_INVARIANT_STMT:
			return processJointInvariantStmt(child);
		default:
			this.reportSyntaxException("Unknown or unimplemented statement: "
					+ node.getText(), node.getChild(0).getLine(), node
					.getChild(0).getCharPositionInLine());
			return null;
		}
	}

	private ASTStatementIF processJointInvariantStmt(CommonTree node)
			throws SyntaxException {
		// Ignore this if doing a verification
		if (configuration instanceof VerifyConfiguration) {
			return new ASTEmptyStatement();
		}
		ASTStatementIF stmt = processCollectiveInvariantStmt(node);
		if (stmt instanceof ASTEmptyStatement) {
			return stmt;
		}
		((ASTAssertStatement) stmt).setInvariant(true);
		((ASTAssertStatement) stmt).setJoint(true);
		return stmt;
	}

	private ASTStatementIF processInvariantStmt(CommonTree node)
			throws SyntaxException {
		ASTIdentifier id = processID((CommonTree) (node.getChild(0)));
		ASTExpressionIF assertion = processExpr((CommonTree) (node.getChild(1)));
		ASTStatementIF stmt = null;
		Source source = null;
		if (!(assertion.getType() instanceof ASTBoolType)) {
			throw new edu.udel.cis.vsl.tass.model.IF.SyntaxException(
					assertion.getSource(), "Assertion must be of boolean type.");
		}
		stmt = new ASTAssertStatement(assertion, id);
		((ASTAssertStatement) stmt).setInvariant(true);
		// Set the source field
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 2));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private ASTStatementIF processCollectiveInvariantStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF stmt = processCollectiveAssertStmt(node);
		if (stmt instanceof ASTEmptyStatement) {
			return stmt;
		}
		((ASTAssertStatement) stmt).setInvariant(true);
		return stmt;
	}

	private ASTStatementIF processJointAssertStmt(CommonTree node)
			throws SyntaxException {
		// Ignore this if doing a verification
		if (configuration instanceof VerifyConfiguration) {
			return new ASTEmptyStatement();
		}
		ASTStatementIF stmt = processCollectiveAssertStmt(node);
		if (stmt instanceof ASTEmptyStatement) {
			return stmt;
		}
		((ASTAssertStatement) stmt).setJoint(true);
		return stmt;
	}

	private ASTStatementIF processCollectiveAssertStmt(CommonTree node)
			throws SyntaxException {
		ASTIdentifier id = processID((CommonTree) (node.getChild(0)));
		ASTExpressionIF assertion = processExpr((CommonTree) (node.getChild(1)));
		ASTStatementIF stmt = null;
		Source source = null;
		if (!(assertion.getType() instanceof ASTBoolType)) {
			throw new edu.udel.cis.vsl.tass.model.IF.SyntaxException(
					assertion.getSource(), "Assertion must be of boolean type.");
		}
		stmt = new ASTAssertStatement(assertion, id);
		((ASTAssertStatement) stmt).setCollective(true);
		// Set the source field
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 2));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private ASTStatementIF processAssertStmt(CommonTree node)
			throws SyntaxException {
		ASTExpressionIF assertion = null;
		assertion = processExpr((CommonTree) (node.getChild(1)));
		ASTStatementIF stmt = null;
		Source source = null;
		String message = null;
		if (!(assertion.getType() instanceof ASTBoolType)) {
			throw new edu.udel.cis.vsl.tass.model.IF.SyntaxException(
					assertion.getSource(), "Assertion must be of boolean type.");
		}
		if (node.getChild(2).getType() != MiniMPLexer.SEMI) {
			message = node.getChild(2).getText()
					.substring(1, node.getChild(2).getText().length() - 1);
			stmt = new ASTAssertStatement(assertion, message);
		} else {
			stmt = new ASTAssertStatement(assertion);
		}
		// Set the source field
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	/*
	 * private StatementIF processAssignmentStmt(CommonTree node) throws
	 * SyntaxException { AssignExpression body = (AssignExpression)
	 * processAssignExpr((CommonTree) (node .getChild(0))); AssignmentStatement
	 * stmt = null; Source source = null;
	 * 
	 * stmt = new AssignmentStatement(body);
	 * 
	 * // Set source for the whole statement source = getSourcePos((CommonTree)
	 * node.getChild(0), (CommonTree) node .getChild(node.getChildCount() - 1));
	 * stmt.setSource(source); stmt.setText(extractSource(source)); return stmt;
	 * }
	 */

	private ASTStatementIF processCompoundStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF stmt = null;
		Source source = null;

		// Only a pair of curly brackets
		if (node.getChildCount() == 2) {
			stmt = new ASTCompoundStatement(new Vector<ASTStatementIF>());
		} else {
			List<ASTStatementIF> stmtList = null;
			stmtList = processStatementList((CommonTree) (node.getChild(1)));
			stmt = new ASTCompoundStatement(stmtList);
		}

		// Set source
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private List<ASTStatementIF> processStatementList(CommonTree node)
			throws SyntaxException {
		List<ASTStatementIF> stmtList = new Vector<ASTStatementIF>();
		for (int i = 0; i < node.getChildCount(); i++) {
			stmtList.add(processStatement((CommonTree) (node.getChild(i))));
		}
		return stmtList;
	}

	private ASTStatementIF processConditionStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF stmt = null;
		Source source = null;

		ASTExpressionIF pred = processExpr((CommonTree) (node.getChild(2)));
		ASTStatementIF trueBranch = processStatement((CommonTree) (node
				.getChild(4)));
		ASTStatementIF falseBranch = null;
		if (node.getChildCount() > 5) {
			falseBranch = processStatement((CommonTree) (node.getChild(6)));
		}
		stmt = new ASTConditionStatement(pred, trueBranch, falseBranch);
		// Set the source
		source = getSourcePos((CommonTree) (node.getChild(0)),
				(CommonTree) (node.getChild(3)));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private ASTStatementIF processSelectStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF stmt = null;
		Source source = null;
		List<ASTSelection> selections = new Vector<ASTSelection>();
		for (int i = 1; i < node.getChildCount(); i++) {
			selections.add(processSelection((CommonTree) (node.getChild(i))));
		}
		stmt = new ASTSelectStatement(selections);
		// Set the source
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private ASTSelection processSelection(CommonTree node)
			throws SyntaxException {
		ASTExpressionIF pred = processExpr((CommonTree) (node.getChild(2)));
		ASTStatementIF action = processStatement((CommonTree) (node.getChild(4)));
		ASTSelection result = new ASTSelection(pred, action);
		Source source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		result.setSource(source);
		result.setText(extractSource(source));
		return result;
	}

	private ASTStatementIF processIterativeStmt(CommonTree node)
			throws SyntaxException {
		ASTLoopInvariant invariant = null;

		if (node.getChildCount() == 1) {
			return processLoopStmt((CommonTree) (node.getChild(0)), invariant);
		} else {
			// Set the corresponding flag in ExecConfig
			if (configuration.useLoopTechnique()) {
				invariant = processLoopInvariant((CommonTree) (node.getChild(0)));
			}
			return processLoopStmt((CommonTree) (node.getChild(1)), invariant);
		}
	}

	private ASTLoopInvariant processLoopInvariant(CommonTree node)
			throws SyntaxException {
		Source source = null;
		ASTLoopInvariant loopInv = null;

		ASTIdentifier id = new ASTIdentifier(node.getChild(0).getText());
		ASTIdentifier function = null;
		// Specify the name of the function where the corresponding loop resides
		// in
		// the other program.
		if (node.getChildCount() == 2) {
			loopInv = new ASTLoopInvariant(id, null, null);
		} else {
			function = new ASTIdentifier(node.getChild(1).getText());
			this.specFunction = function;
			int spec = 1;
			int impl = 1;
			ASTExpressionIF invariant = null;

			if (node.getChildCount() == 4) {
				invariant = processExpr((CommonTree) (node.getChild(2)));
				loopInv = new ASTLoopInvariant(id, function, invariant);
			} else {
				// There is a skew factor
				spec = Integer.valueOf(node.getChild(2).getChild(0).getText())
						.intValue();
				impl = Integer.valueOf(node.getChild(2).getChild(1).getText())
						.intValue();
				invariant = processExpr((CommonTree) (node.getChild(3)));
				loopInv = new ASTLoopInvariant(id, function, invariant, spec,
						impl);
			}
		}
		// Set the source
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		loopInv.setSource(source);
		loopInv.setText(extractSource(source));
		this.specFunction = null;
		return loopInv;
	}

	private ASTStatementIF processLoopStmt(CommonTree node,
			ASTLoopInvariant invariant) throws SyntaxException {
		ASTStatementIF stmt = null;
		Source source = null;

		if (node.getType() == MiniMPLexer.WHILE_STMT) {
			ASTExpressionIF pred = processExpr((CommonTree) (node.getChild(2)));
			ASTStatementIF body = processStatement((CommonTree) (node
					.getChild(4)));
			stmt = new ASTWhileStatement(pred, body, invariant);
			// Set the source
			source = getSourcePos((CommonTree) node.getChild(0),
					(CommonTree) node.getChild(3));
			stmt.setSource(source);
			stmt.setText(extractSource(source));
		} else if (node.getType() == MiniMPLexer.FOR_STMT) {
			ASTExpressionIF init = null;
			ASTExpressionIF pred = null;
			ASTExpressionIF update = null;
			ASTStatementIF body = processStatement((CommonTree) (node
					.getChild(node.getChildCount() - 1)));

			if (node.getChildCount() == 6) {
				// for(init; ;)
				if (node.getChild(1).getType() != MiniMPLexer.SEMI) {
					init = processExpr((CommonTree) (node.getChild(1)));
				}
				// for(; pred; )
				else if (node.getChild(2).getType() != MiniMPLexer.SEMI) {
					pred = processExpr((CommonTree) (node.getChild(2)));
				}
				// for(; ; update)
				else if (node.getChild(3).getType() != MiniMPLexer.RPAREN) {
					update = processExpr((CommonTree) (node.getChild(3)));
				} else {
					this.reportSyntaxException(
							"Incorrect FOR statement structure.",
							node.getLine(), node.getCharPositionInLine());
				}
			} else if (node.getChildCount() == 7) {
				// for(init; pred; )
				if (node.getChild(2).getType() == MiniMPLexer.SEMI
						&& node.getChild(4).getType() == MiniMPLexer.SEMI) {
					init = processExpr((CommonTree) (node.getChild(1)));
					pred = processExpr((CommonTree) (node.getChild(3)));
				}
				// for( ; pred; update)
				else if (node.getChild(1).getType() == MiniMPLexer.SEMI
						&& node.getChild(3).getType() == MiniMPLexer.SEMI) {
					pred = processExpr((CommonTree) (node.getChild(2)));
					update = processExpr((CommonTree) (node.getChild(4)));
				}
				// for(init; ; update)
				else if (node.getChild(2).getType() == MiniMPLexer.SEMI
						&& node.getChild(3).getType() == MiniMPLexer.SEMI) {
					init = processExpr((CommonTree) (node.getChild(1)));
					update = processExpr((CommonTree) (node.getChild(3)));
				}
			}
			// for(init; pred; update)
			else if (node.getChildCount() == 8) {
				init = processExpr((CommonTree) (node.getChild(1)));
				pred = processExpr((CommonTree) (node.getChild(3)));
				update = processExpr((CommonTree) (node.getChild(5)));
			}
			stmt = new ASTForStatement(init, pred, update, body, invariant);
			// Set the source
			source = this.getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 2)));
			stmt.setSource(source);
			stmt.setText(this.extractSource(source));
		} else {
			this.reportSyntaxException(
					"Statement not implemented: " + node.getText(),
					node.getLine(), node.getCharPositionInLine());
		}

		return stmt;
	}

	private ASTStatementIF processReturnStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF stmt = null;
		Source source = null;

		// should this be 0?

		int numChildren = node.getChildCount();

		if (numChildren <= 2) {
			// 2 because one child is the "RETURN" and the second is the
			// semicolon
			assert numChildren == 2;
			stmt = new ASTReturnStatement(null);
		} else {
			// should have 3 children: the third is the semicolon
			assert numChildren == 3;
			stmt = new ASTReturnStatement(
					processExpr((CommonTree) (node.getChild(1))));
		}
		// Set the source
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(numChildren - 1));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private ASTStatementIF processEmptyStmt(CommonTree node) {
		return new ASTEmptyStatement();
	}

	private ASTStatementIF processSendStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF stmt = null;
		Source source = null;

		ASTExpressionIF temp = processExpr((CommonTree) (node.getChild(1)));
		if (!(temp instanceof ASTBufferExpressionIF)) {
			/*
			 * throw new RuntimeException(
			 * "The first argument of send statement must be of type BufferExpressionIF."
			 * );
			 */
			this.reportSyntaxException(
					"The first argument of send statement must be of type BufferExpressionIF.",
					node.getChild(1).getLine(), node.getChild(1)
							.getCharPositionInLine());
		}

		ASTBufferExpressionIF data = (ASTBufferExpressionIF) temp;

		ASTExpressionIF dest = processExpr((CommonTree) (node.getChild(2)));
		ASTExpressionIF tag = processExpr((CommonTree) (node.getChild(3)));
		stmt = new ASTSendStatement(data, dest, tag);
		// Set the source
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private ASTStatementIF processRecvStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF stmt = null;
		Source source = null;

		ASTExpressionIF temp = processExpr((CommonTree) (node.getChild(1)));
		if (!(temp instanceof ASTBufferExpressionIF)) {
			this.reportSyntaxException(
					"The first argument of receive statement must be of type BufferExpressionIF.",
					node.getChild(1).getLine(), node.getChild(1)
							.getCharPositionInLine());
		}

		ASTBufferExpressionIF data = (ASTBufferExpressionIF) temp;
		ASTExpressionIF src = processCommunicationExpr((CommonTree) (node
				.getChild(2)));
		ASTExpressionIF tag = processCommunicationExpr((CommonTree) (node
				.getChild(3)));
		if (node.getChildCount() == 5) {
			stmt = new ASTReceiveStatement(data, src, tag);
		} else {
			ASTLhsExpressionIF size = (ASTLhsExpressionIF) processUnaryExpr((CommonTree) node
					.getChild(4));
			stmt = new ASTReceiveStatement(data, src, tag, size);
		}
		// Set the source
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private ASTExpressionIF processCommunicationExpr(CommonTree node)
			throws SyntaxException {
		CommonTree child = (CommonTree) (node.getChild(0));
		ASTExpressionIF expr = null;
		Source source = null;

		if (child.getType() == MiniMPLexer.EXPR) {
			return processExpr(child);
		} else {
			expr = new ASTWildcardExpression(
					processExpr((CommonTree) (child.getChild(2))));
			// Set the source
			source = getSourcePos((CommonTree) (node.getChild(0)),
					(CommonTree) (node.getChild(node.getChildCount() - 1)));
			expr.setSource(source);
			expr.setText(extractSource(source));
			return expr;
		}
	}

	private ASTStatementIF processAssumeStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF stmt = null;
		Source source = null;
		stmt = new ASTAssumeStatement(
				processExpr((CommonTree) (node.getChild(1))));
		// Set the source field
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private ASTStatementIF processAllocateStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF stmt = null;
		Source source = null;
		ASTLhsExpressionIF lhs = (ASTLhsExpressionIF) processUnaryExpr((CommonTree) node
				.getChild(0));
		ASTTypeIF type = processTypeName((CommonTree) node.getChild(1));
		ASTExpressionIF size = processUnaryExpr((CommonTree) node.getChild(2));
		stmt = new ASTAllocateStatement(lhs, type, size);
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private ASTStatementIF processCallStmt(CommonTree node)
			throws SyntaxException {
		ASTLhsExpressionIF lhs = null;
		ASTIdentifier name = null;
		List<ASTExpressionIF> paramList = new Vector<ASTExpressionIF>();
		CommonTree child = (CommonTree) (node.getChild(0));
		ASTExpressionIF temp = null;
		ASTStatementIF stmt = null;
		Source source = null;

		// No lhs
		if (child.getType() == MiniMPLexer.IDENTIFIER) {
			name = processID(child);
			//TODO: Handle printf correctly
			if (name.toString().equals("printf")) {
				return new ASTEmptyStatement();
			}
			if (node.getChildCount() == 5) {
				paramList = processParamList((CommonTree) (node.getChild(2)));
			}
		}
		// With lhs
		else {
			name = processID((CommonTree) (node.getChild(1)));
			if (name.toString().equals("printf")) {
				return new ASTEmptyStatement();
			}
			temp = this.processUnaryExpr(child);
			if (!(temp instanceof ASTLhsExpressionIF)) {
				this.reportSyntaxException(
						"The left hand side of an invocation statement must be a left hand side expression.",
						child.getLine(), child.getCharPositionInLine());
			} else {
				lhs = (ASTLhsExpressionIF) temp;
			}
			if (node.getChildCount() == 6) {
				paramList = processParamList((CommonTree) (node.getChild(3)));
			}
		}

		stmt = new ASTInvocationStatement(lhs, name.toString(), paramList);

		// Set the source
		source = getSourcePos((CommonTree) node.getChild(0),
				(CommonTree) node.getChild(node.getChildCount() - 1));
		stmt.setSource(source);
		stmt.setText(extractSource(source));
		return stmt;
	}

	private List<ASTExpressionIF> processParamList(CommonTree node)
			throws SyntaxException {
		List<ASTExpressionIF> paramList = new Vector<ASTExpressionIF>();
		for (int i = 0; i < node.getChildCount(); i++) {
			paramList.add(processParameter((CommonTree) (node.getChild(i))));
		}
		return paramList;
	}

	private ASTExpressionIF processParameter(CommonTree node)
			throws SyntaxException {
		return processExpr((CommonTree) (node.getChild(0)));
	}

	private ASTStatementIF processExprStmt(CommonTree node)
			throws SyntaxException {
		ASTStatementIF result = null;
		ASTExpressionIF expr = processExpr((CommonTree) (node.getChild(0)));
		if (expr instanceof ASTAssignExpression) {
			result = new ASTAssignmentStatement((ASTAssignExpression) expr);
		}
		// i++ -> i = i + 1
		// i-- -> i = i - 1;
		else if (expr instanceof ASTSelfChangeExpression) {
			ASTSelfChangeExpression temp = (ASTSelfChangeExpression) expr;
			if (temp.getOperator() == SelfChangeOperator.INCREMENT) {
				expr = new ASTAssignExpression(
						(ASTLhsExpressionIF) (temp.getBody()),
						new ASTBinaryExpression(
								BinaryOperator.PLUS,
								(ASTLhsExpressionIF) (temp.getBody()),
								new ASTIntegerLiteral(new ASTIntegerType(), "1")));
			} else {
				expr = new ASTAssignExpression(
						(ASTLhsExpressionIF) (temp.getBody()),
						new ASTBinaryExpression(
								BinaryOperator.SUB,
								(ASTLhsExpressionIF) (temp.getBody()),
								new ASTIntegerLiteral(new ASTIntegerType(), "1")));
			}
			result = new ASTAssignmentStatement((ASTAssignExpression) expr);
		} else {
			this.reportSyntaxException(
					"Only assign or increment/decrement expressions are allowed in expression statement.",
					node.getChild(0).getLine(), node.getChild(0)
							.getCharPositionInLine());
		}
		Source source = getSourcePos((CommonTree) (node.getChild(0)),
				(CommonTree) (node.getChild(node.getChildCount() - 1)));
		result.setSource(source);
		result.setText(extractSource(source));
		return result;
	}

	/*
	 * private StatementIF processAllocateStmt(CommonTree node) throws
	 * SyntaxException { ExpressionIF buffer =
	 * this.processUnaryExpr((CommonTree)(node.getChild(1))); TypeIF elementType
	 * = null; ExpressionIF elementCount = null; ExpressionIF typeExpr = null;
	 * 
	 * if(node.getChildCount() == 5) { elementCount =
	 * processExpr((CommonTree)(node.getChild(2))); typeExpr =
	 * this.processUnaryExpr((CommonTree)(node.getChild(3))); } else {
	 * elementCount = new IntegerLiteral(new IntegerType(), "1"); typeExpr =
	 * this.processUnaryExpr((CommonTree)(node.getChild(2))); }
	 * 
	 * if(!(typeExpr instanceof SizeofExpression)) {this.reportSyntaxException(
	 * "The type expression in a malloc call must be a sizeof expression.",
	 * node.getLine(), node.getCharPositionInLine()); }
	 * 
	 * StatementIF result = new AllocateStatement(buffer, elementType,
	 * elementCount);
	 * 
	 * //source Source source = new Source(this.file,
	 * node.getChild(0).getLine(), node.getChild(node.getChildCount() -
	 * 1).getLine(), node.getChild(0).getCharPositionInLine(),
	 * node.getChild(node.getChildCount() - 1).getCharPositionInLine());
	 * result.setSource(source); result.setText(extractSource(source)); return
	 * result; }
	 */

	/*
	 * private StatementIF processDeallocateStmt(CommonTree node) throws
	 * SyntaxException { ExpressionIF buffer =
	 * processExpr((CommonTree)(node.getChild(1))); StatementIF result = new
	 * DeallocateStatement(buffer); //source Source source = new
	 * Source(this.file, node.getChild(0).getLine(),
	 * node.getChild(node.getChildCount() - 1).getLine(),
	 * node.getChild(0).getCharPositionInLine(),
	 * node.getChild(node.getChildCount() - 1).getCharPositionInLine());
	 * result.setSource(source); result.setText(extractSource(source)); return
	 * result; }
	 */

	/* Get the coordinates of the source code. */
	private Source getSourcePos(CommonTree startNode, CommonTree lastNode) {
		int startLine = startNode.getLine();
		int startCol = startNode.getCharPositionInLine();
		this.findLastLineAndColumn(lastNode);
		int endLine = this.lastLine;
		int endCol = this.lastColumn;
		this.lastLine = 0;
		this.lastColumn = 0;
		return new Source(this.file, startLine, endLine, startCol, endCol);
	}

	/*
	 * Get the actual source code specified by the source object from the source
	 * file
	 */
	private String extractSource(Source source) {
		BufferedReader reader = null;
		StringBuffer result = new StringBuffer();

		try {
			reader = new BufferedReader(new FileReader(this.file));
			int lineNum = 1;
			while (lineNum < source.firstLine()) {
				reader.readLine();
				lineNum++;
			}
			if (source.firstLine() != source.lastLine()) {
				result.append(reader.readLine().substring(source.firstColumn()));
				lineNum++;
				while (lineNum < source.lastLine()) {
					result.append(reader.readLine());
					lineNum++;
				}
				String temp = reader.readLine();
				result.append(temp.substring(0, source.lastColumn()));
			} else {
				result.append(reader.readLine().substring(source.firstColumn(),
						source.lastColumn()));
			}

			for (int i = 0; i < result.length(); i++) {
				if (result.charAt(i) == '\t') {
					result = result.deleteCharAt(i);
					i--;
				}
			}

			for (int i = result.length() - 1; i >= 0; i--) {
				if (result.charAt(i) == ' ') {
					result = result.deleteCharAt(i);
				} else {
					break;
				}
			}
		} catch (IOException e) {
			System.err.println(e);
			if (reader != null) {
				try {
					reader.close();
				} catch (Exception ex) {
					System.err.println(ex);
				}
			}
		}
		try {
			reader.close();
		} catch (IOException e) {
			System.err.println(e);
		}
		return result.toString();
	}

	private void findLastLineAndColumn(CommonTree node) {
		CommonTree temp = node;
		while (temp.getChildCount() != 0) {
			temp = (CommonTree) (temp.getChild(temp.getChildCount() - 1));
		}
		this.lastLine = temp.getLine();
		this.lastColumn = temp.getCharPositionInLine()
				+ temp.getText().length();
	}

	private ASTFunctionDeclaration checkReturn(ASTFunctionDeclaration function,
			CommonTree child) {
		if (function.getBody() == null)
			return function;
		if (!(function.getType() instanceof ASTVoidType)) {
			return function;
		} else {
			List<ASTStatementIF> stmtList = new Vector<ASTStatementIF>(function
					.getBody().getStatementList());
			// adding implicit return statement.
			ASTStatementIF stmt = new ASTReturnStatement(null);
			CommonTree node = (CommonTree) child
					.getChild(child.getChildCount() - 1);
			Source source = function.source();
			Source newSource = new Source(source.file(), node.getLine(),
					node.getLine(), node.getCharPositionInLine(),
					node.getCharPositionInLine());
			newSource.setText("}");
			// stmt.setSource(this.lastPosition);
			stmt.setSource(newSource);
			this.lastPosition = null;
			stmtList.add(stmt);
			Map<String, ASTDeclarationIF> varMap = new LinkedHashMap<String, ASTDeclarationIF>(
					function.getBody().getLocalVariableMap());
			ASTFunction newBody = new ASTFunction(varMap, stmtList);
			function.setBody(newBody);
			return function;
		}
	}

	private void reportSyntaxException(String message, int line, int column)
			throws SyntaxException {
		String errorMsg = "Syntax error found in file: " + this.file.getName()
				+ ", on line: " + line + ":" + column + "\n";
		errorMsg += message;
		throw new SyntaxException(errorMsg);
	}

	// Takes a struct type and an index list, make necessary changes to the
	// index list
	// so that it contains the correct indices to the next field.
	private Vector<Integer> findNextField(ASTStructType type, CommonTree node,
			Vector<Integer> indexList) throws SyntaxException {
		if (indexList.size() == 1) {
			int fieldIndex = indexList.remove(0);
			fieldIndex++;
			if (type.getFieldType(fieldIndex) != null) {
				indexList.add(fieldIndex);
				if (type.getFieldType(fieldIndex) instanceof ASTArrayType
						|| type.getFieldType(fieldIndex) instanceof ASTStructType) {
					ASTTypeIF temp = type.getFieldType(fieldIndex);
					while (temp instanceof ASTArrayType
							|| temp instanceof ASTStructType) {
						indexList.add(0);
						if (temp instanceof ASTArrayType) {
							temp = ((ASTArrayType) temp).getBaseType();
						} else {
							temp = ((ASTStructType) temp).getFieldType(0);
						}
					}
				}
				return indexList;
			} else {
				return null;
			}
		} else {
			ASTTypeIF fieldType = type.getFieldType(indexList.get(0));
			if (fieldType instanceof ASTArrayType
					|| fieldType instanceof ASTStructType) {
				Vector<Integer> newList = new Vector<Integer>();
				while (indexList.size() > 1) {
					newList.add(indexList.remove(1));
				}
				Vector<Integer> resultList = null;
				if (fieldType instanceof ASTArrayType) {
					resultList = this.findNextElement((ASTArrayType) fieldType,
							node, newList);
				} else {
					resultList = this.findNextField((ASTStructType) fieldType,
							node, newList);
				}
				if (resultList == null) {
					int fieldIndex = indexList.remove(0);
					fieldIndex++;
					if (type.getFieldType(fieldIndex) != null) {
						indexList.add(fieldIndex);
						if (type.getFieldType(fieldIndex) instanceof ASTArrayType
								|| type.getFieldType(fieldIndex) instanceof ASTStructType) {
							ASTTypeIF temp = type.getFieldType(fieldIndex);
							while (temp instanceof ASTArrayType
									|| temp instanceof ASTStructType) {
								indexList.add(0);
								if (temp instanceof ASTArrayType) {
									temp = ((ASTArrayType) temp).getBaseType();
								} else {
									temp = ((ASTStructType) temp)
											.getFieldType(0);
								}
							}
						}
						return indexList;
					} else {
						return null;
					}
				} else {
					indexList.addAll(resultList);
					return indexList;
				}
			} else {
				this.reportSyntaxException(
						"Struct or array type expected instead of " + fieldType,
						node.getLine(), node.getCharPositionInLine());
				return null;
			}
		}
	}

	// Takes an array type and an index list and makes necessary changes to the
	// list to represent the next element
	// in the array.
	private Vector<Integer> findNextElement(ASTArrayType type, CommonTree node,
			Vector<Integer> indexList) throws SyntaxException {
		List<Integer> dimensionList = new Vector<Integer>();
		ASTTypeIF temp = type;
		while (temp instanceof ASTArrayType) {
			dimensionList.add(Integer
					.valueOf(((ASTIntegerLiteral) (((ASTArrayType) temp)
							.getLength())).getValue()));
			temp = ((ASTArrayType) temp).getBaseType();
		}

		if (indexList.size() == dimensionList.size()) {
			// Increase array indices
			for (int i = dimensionList.size() - 1; i >= 0; i--) {
				int index = indexList.get(i);
				index++;
				if (index == dimensionList.get(i)) {
					if (i > 0) {
						indexList.setElementAt(0, i);
					} else {
						return null;
					}
				} else {
					indexList.setElementAt(index, i);
					return indexList;
				}
			}
		} else if (indexList.size() > dimensionList.size()) {
			if (temp instanceof ASTStructType) {
				Vector<Integer> newList = new Vector<Integer>();
				while (indexList.size() > dimensionList.size()) {
					dimensionList
							.add(indexList.remove(dimensionList.size() - 1));
				}
				Vector<Integer> resultList = this.findNextField(
						(ASTStructType) temp, node, newList);
				if (resultList == null) {
					// Increase array indices
					for (int i = dimensionList.size() - 1; i >= 0; i--) {
						int index = indexList.get(i);
						index++;
						if (index == dimensionList.get(i)) {
							if (i > 0) {
								indexList.add(i, 0);
							} else {
								return null;
							}
						}
					}

					while (temp instanceof ASTStructType) {
						indexList.add(0);
						temp = ((ASTStructType) temp).getFieldType(0);
					}
				} else {
					indexList.addAll(resultList);
				}
				return indexList;
			} else {
				this.reportSyntaxException("Struct type expected instead of "
						+ temp, node.getLine(), node.getCharPositionInLine());
			}
		} else {
			this.reportSyntaxException(
					"Index list can not have fewer elements than dimension list.",
					node.getLine(), node.getCharPositionInLine());
		}
		return null;
	}

	@Override
	public void addSystemDeclaration(ASTDeclarationIF aDeclaration) {
		// TODO Auto-generated method stub

	}
}

class NameTypePair {
	private ASTIdentifier name;
	private ASTTypeIF type;

	public NameTypePair(ASTIdentifier name, ASTTypeIF type) {
		if (name == null) {
			throw new RuntimeException("Name can not be null.");
		}
		if (type == null) {
			throw new RuntimeException("Type can not be null.");
		}
		this.name = name;
		this.type = type;
	}

	public ASTIdentifier getName() {
		return this.name;
	}

	public ASTTypeIF getType() {
		return this.type;
	}
}