import gov.nasa.jpf.util.TypeRef;
import gov.nasa.jpf.util.test.TestJPF;

import org.junit.Test;

/**
 * Some basic tests for JPF.
 *
 * @author Franck van Breugel
 */
public class BasicTest extends TestJPF {
	/**
	 * JPF's application properties.
	 */
	private static String[] PROPERTIES = { "+classpath=C:/users/franck/workspace/project/bin/", "+@include=C:/users/franck/jpf/jpf-core/jpf.properties" };

	/**
	 * Tests whether JPF detects an assertion error.
	 */
	@Test
	public void assertTest() {
		if (this.verifyAssertionError(BasicTest.PROPERTIES)) {
			assert false;
		} 
	}

	/**
	 * Tests whether JPF detects an unhandled exception.
	 */
	@Test
	public void exceptionTest() {
		if (this.verifyUnhandledException("java.lang.NullPointerException", 
				BasicTest.PROPERTIES)) {
			throw new NullPointerException();
		}
	}

	/**
	 * Tests whether JPF detects a violation of the property NoUncaughtExceptionsProperty.
	 */
	@Test
	public void propertyViolationTest() {
		if (this.verifyPropertyViolation(new TypeRef("gov.nasa.jpf.vm.NoUncaughtExceptionsProperty"), 
				BasicTest.PROPERTIES)) {
			throw new RuntimeException();
		}
	}

	/**
	 * Tests whether JPF detects that no property has been violated.
	 */
	@Test
	public void noPropertyViolationTest() {
		if (this.verifyNoPropertyViolation(BasicTest.PROPERTIES)) {
			// nothing
		}
	}

	/**
	 * Runs the test methods with the given names.  If no names are given, all test methods are run.
	 *
	 * @param testMethods the names of the test methods to be run.
	 */
	public static void main(String[] testMethods) {
		TestJPF.runTestsOfThisClass(testMethods);
	}
}