AssumeStatement.java

package edu.udel.cis.vsl.tass.model.impl.statement;

import java.util.Collection;

import edu.udel.cis.vsl.tass.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.SyntaxException;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.location.AssumeLocationIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssumeStatementIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF.TypeKind;
import edu.udel.cis.vsl.tass.model.IF.variable.SharedVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.VariableIF;

public class AssumeStatement extends Statement implements AssumeStatementIF {

	private ExpressionIF assumption;

	public AssumeStatement(ModelFactoryIF factory,
			AssumeLocationIF sourceLocation, ExpressionIF assumption)
			throws SyntaxException {
		/*
		 * The reason we make the assumption the guard is that if the assumption
		 * is invalid under the path condition then we will not even execute
		 * this assume: so there is no need for special code to indicate a back
		 * track.
		 */
		super(factory, assumption, sourceLocation, StatementKind.ASSUME);
		if (assumption == null)
			throw new NullPointerException("Null assumption");
		if (assumption.type().kind() != TypeKind.BOOLEAN)
			throw new SyntaxException(assumption,
					"Type of assertion expression is not boolean");
		factory.checkScope(assumption, sourceLocation.scope());
		this.assumption = assumption;
	}

	public String toString() {
		return "assume " + assumption + ";";
	}

	public ExpressionIF assumption() {
		return assumption;
	}

	public void complete() throws SyntaxException {
		Collection<SharedVariableIF> shared = process().model().scope()
				.properSharedVariables();

		super.complete();
		isLocal = true;
		for (VariableIF variable : assumption.freeVariables()) {
			if (variable instanceof SharedVariableIF
					&& shared.contains((SharedVariableIF) variable)) {
				isLocal = false;
				break;
			}
		}
	}
}