Throw exception when testsuite does not support skipping tests

ultimate-pa · Aug 20, 2024 · aba9b93 · aba9b93
1 parent 895ac12
commit aba9b93
Show file tree

Hide file tree

Showing 13 changed files with 39 additions and 11 deletions.
diff --git a/...t/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java b/...t/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java
@@ -335,6 +335,12 @@ protected Collection<File> getInputFiles(final Predicate<File> regexFilter, fina
 	protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition,
 			String overridenExpectedVerdict);
 
+	protected void checkNoOverridenVerdict(final String overridenExpectedVerdict) {
+		if (overridenExpectedVerdict != null) {
+			throw new UnsupportedOperationException(getClass().getSimpleName() + " does not support skipping tests.");
+		}
+	}
+
 	public static final class Config
 			extends de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair<File, File> {
 

diff --git a/...tik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java b/...tik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java
@@ -46,7 +46,9 @@ public BoogieBacktranslationRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new BacktranslationTestResultDecider(runDefinition);
 	}
 }
diff --git a/...formatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java b/...formatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java
@@ -46,7 +46,9 @@ public CBacktranslationRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new BacktranslationTestResultDecider(runDefinition);
 	}
 }
diff --git a/...de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java b/...de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java
@@ -51,7 +51,9 @@ public AbsIntRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new OverapproximatingSafetyCheckTestResultDecider(runDefinition, true);
 	}
 }
diff --git a/...eiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java b/...eiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java
@@ -50,7 +50,9 @@ public AutomataLibraryRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new AutomataScriptTestResultDecider();
 	}
 

diff --git a/...rc/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java b/...rc/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java
@@ -57,8 +57,10 @@ public ChcRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
-		boolean unknownIsSuccess = false;
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
+		final boolean unknownIsSuccess = false;
 		return new ChcTestResultDecider(runDefinition, unknownIsSuccess);
 	}
 }
diff --git a/.../uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java b/.../uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java
@@ -56,7 +56,9 @@ public DataRaceRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new SafetyCheckTestResultDecider(runDefinition, false);
 	}
 

diff --git a/...rc/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java b/...rc/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java
@@ -49,7 +49,9 @@ public LTLRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new LTLCheckerTestResultDecider(runDefinition, false);
 	}
 

diff --git a/...c/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java b/...c/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java
@@ -51,7 +51,9 @@ public MSODRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		final boolean unknownIsSuccess = true;
 		return new MSODTestResultDecider(runDefinition, unknownIsSuccess);
 	}

diff --git a/...g/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java b/...g/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java
@@ -78,6 +78,7 @@ public ReqCheckerRedundancyRegressionTestSuite() {
 	@Override
 	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
 			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new ReqCheckerTestResultDecider(runDefinition, false);
 	}
 

diff --git a/...ni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java b/...ni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java
@@ -79,7 +79,9 @@ public ReqCheckerRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new ReqCheckerTestResultDecider(runDefinition, false);
 	}
 

diff --git a/...i_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java b/...i_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java
@@ -50,7 +50,9 @@ public TerminationRegressionTestSuite() {
 	}
 
 	@Override
-	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) {
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new TerminationAnalysisTestResultDecider(runDefinition, false);
 	}
 

diff --git a/...e/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java b/...e/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java
@@ -63,6 +63,7 @@ public WitnessRegressionTestSuite() {
 	@Override
 	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
 			final String overridenExpectedVerdict) {
+		checkNoOverridenVerdict(overridenExpectedVerdict);
 		return new WitnessSafetyCheckTestResultDecider(runDefinition);
 	}