package de.fzi.cjunit.jpf.assumptions;

import static org.hamcrest.MatcherAssert.assertThat;
import static org.hamcrest.Matchers.*;

import java.util.List;

import gov.nasa.jpf.Error;
import gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty;

import org.junit.Test;

import de.fzi.cjunit.testutils.JPFForTesting;

/*
 * JPF provides its own implementation of some standard Java classes, but
 * those implementations are in some cases incomplete, i.e. there are methods
 * missing from the JPF implementation that are part of the public API or the
 * originals.  This class collects some of those methods.
 */
public class NoSuchMethodExceptionInJPF extends JPFForTesting {

	public static class GT {
		public static void main(String[] args) {
			assertThat(0, greaterThan(1));
		}
	}

	public static class GTOE {
		public static void main(String[] args) {
			assertThat(0, greaterThanOrEqualTo(1));
		}
	}

	public static class LT {
		public static void main(String[] args) {
			assertThat(1, lessThan(0));
		}
	}

	public static class LTOE {
		public static void main(String[] args) {
			assertThat(1, lessThanOrEqualTo(0));
		}
	}

	public void runTest(Class<?> app, Class<? extends Throwable> tc) {
		createJPF(app);
		NoUncaughtExceptionsProperty nuep
				= new NoUncaughtExceptionsProperty(config);
		jpf.addSearchProperty(nuep);
		jpf.run();
		List<Error> errors = jpf.getSearchErrors();
		assertThat("number of errors", errors.size(), equalTo(1));
		assertThat("exception type",
				nuep.getUncaughtExceptionInfo().getExceptionClassname(),
				equalTo(tc.getName()));
	}

	@Test
	public void testGT() {
		runTest(GT.class, AssertionError.class);
	}

	@Test
	public void testGTOE() {
		runTest(GTOE.class, NoSuchMethodException.class);
	}

	@Test
	public void testLT() {
		runTest(LT.class, NoSuchMethodException.class);
	}

	@Test
	public void testLTOE() {
		runTest(LTOE.class, NoSuchMethodException.class);
	}
}

Add test to show "surprising" NoSuchMethodExceptions in JPF
Add test to show "surprising" NoSuchMethodExceptions in JPF

JPF provides its own implementation of some standard Java classes, but
those implementations are in some cases incomplete, i.e. there are
methods missing from the JPF implementation that are part of the
public API or the originals.  This assumption test class collects some
of those methods.

Signed-off-by: SZEDER Gábor <46692b1f0516358b02a6405518c0a52aa8fb3e94@fzi.de>
