Only allow skip files next to the tests itself

trunk/examples/programs/regression/bpl/skip.yml

@@ -34,12 +34,3 @@ unknown symbol (@diff:
 - task: BugLiveVariables04-Safe.bpl
   settings: AutomizerBpl-nestedInterpolants.epf
   toolchain: AutomizerBpl.xml
-
-# Issue in SMTInterpol
-Const is only supported for infinite index sort:
-- task: ConstArray.bpl
-  settings: AutomizerBpl-nestedInterpolants.epf
-  toolchain: AutomizerBpl.xml
-- task: ConstArray.bpl
-  settings: AutomizerBpl-nestedInterpolants.epf
-  toolchain: PdrAutomizerBpl.xml

trunk/examples/programs/regression/bpl/toolDirectives/skip.yml

@@ -0,0 +1,8 @@
+# Issue in SMTInterpol
+Const is only supported for infinite index sort:
+- task: ConstArray.bpl
+  settings: AutomizerBpl-nestedInterpolants.epf
+  toolchain: AutomizerBpl.xml
+- task: ConstArray.bpl
+  settings: AutomizerBpl-nestedInterpolants.epf
+  toolchain: PdrAutomizerBpl.xml

trunk/examples/programs/regression/c/interprocedural/skip.yml

@@ -0,0 +1,10 @@
+TIMEOUT:
+- task: Acsl01-EnsuresLocal-Safe.c
+  settings: AutomizerC-BitvectorTranslation.epf
+  toolchain: AutomizerC.xml
+- task: Acsl03-EnsuresGlobal-Safe.c
+  settings: AutomizerC-BitvectorTranslation.epf
+  toolchain: AutomizerC.xml
+- task: Tschingelhorn-Safe.c
+  settings: AutomizerC-BitvectorTranslation.epf
+  toolchain: AutomizerC.xml

trunk/examples/programs/regression/c/skip.yml

@@ -116,15 +116,6 @@ TIMEOUT:
 - task: builtin_ffs.c
   settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf
   toolchain: BlockEncodingV2AutomizerC.xml
-- task: Acsl01-EnsuresLocal-Safe.c
-  settings: AutomizerC-BitvectorTranslation.epf
-  toolchain: AutomizerC.xml
-- task: Acsl03-EnsuresGlobal-Safe.c
-  settings: AutomizerC-BitvectorTranslation.epf
-  toolchain: AutomizerC.xml
-- task: Tschingelhorn-Safe.c
-  settings: AutomizerC-BitvectorTranslation.epf
-  toolchain: AutomizerC.xml
 
 unable to decide satisfiability of path constraint:
 - task: array10_pattern_simplified.c

trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java

@@ -117,41 +117,42 @@ public Collection<UltimateTestCase> createTestCases() {
 		final Predicate<File> filesRegexFilter = getFilesRegexFilter();
 		for (final Config runConfiguration : runConfigurations) {
 			final Collection<File> inputFiles = getInputFiles(filesRegexFilter, runConfiguration);
-			final NestedMap3<String, String, String, String> skippedTests = getSkippedTests(runConfiguration);
+			final NestedMap3<File, String, String, String> skippedTests = getSkippedTests(inputFiles);
 			for (final File inputFile : inputFiles) {
 				final UltimateRunDefinition urd =
 						new UltimateRunDefinition(inputFile, runConfiguration.getSettingsFile(),
 								runConfiguration.getToolchainFile(), getTimeout(runConfiguration, inputFile));
-				final String overridenVerdict = skippedTests.get(inputFile.getName(),
+				final String overridenVerdict = skippedTests.get(inputFile,
 						runConfiguration.getSettingsFile().getName(), runConfiguration.getToolchainFile().getName());
 				rtr.add(buildTestCase(urd, getTestResultDecider(urd, overridenVerdict)));
 			}
 		}
 		return rtr;
 	}
 
-	private static NestedMap3<String, String, String, String> getSkippedTests(final Config runConfiguration) {
-		final NestedMap3<String, String, String, String> result = new NestedMap3<>();
-		final File settingsDir = runConfiguration.getSettingsFile().getParentFile();
-		final File toolchainDir = runConfiguration.getToolchainFile().getParentFile();
-		if (settingsDir.equals(toolchainDir)) {
-			addSkippedTest(new File(settingsDir, SKIPPED_FILENAME), result);
-		} else if (settingsDir.toString().length() < toolchainDir.toString().length()) {
-			addSkippedTest(new File(settingsDir, SKIPPED_FILENAME), result);
-			addSkippedTest(new File(toolchainDir, SKIPPED_FILENAME), result);
-		} else {
-			addSkippedTest(new File(toolchainDir, SKIPPED_FILENAME), result);
-			addSkippedTest(new File(settingsDir, SKIPPED_FILENAME), result);
-		}
+	/**
+	 * Collect all tests that should be marked as skipped. To do so, all files with SKIPPED_FILENAME next to
+	 * {@code inputFiles} are considered and a NestedMap3 is extracted from.
+	 */
+	private static NestedMap3<File, String, String, String> getSkippedTests(final Collection<File> inputFiles) {
+		final NestedMap3<File, String, String, String> result = new NestedMap3<>();
+		inputFiles.stream().map(x -> new File(x.getParentFile(), SKIPPED_FILENAME)).distinct()
+				.forEach(x -> addSkippedTest(x, result));
 		return result;
 	}
 
-	private static void addSkippedTest(final File ignoreFile, final NestedMap3<String, String, String, String> map) {
+	private static void addSkippedTest(final File ignoreFile, final NestedMap3<File, String, String, String> map) {
 		try {
 			final Map<String, List<Map<String, String>>> parsed = new Yaml().load(new FileInputStream(ignoreFile));
 			for (final var entry : parsed.entrySet()) {
 				for (final Map<String, String> triples : entry.getValue()) {
-					map.put(triples.get("task"), triples.get("settings"), triples.get("toolchain"), entry.getKey());
+					if (triples.values().stream().anyMatch(x -> x.contains("/"))) {
+						throw new UnsupportedOperationException("Invalid filename in ignore-file" + ignoreFile
+								+ ". The filename may only contain a name, not a relative path. "
+								+ "Add a new ignore-file next to the task itself (if desired).");
+					}
+					map.put(new File(ignoreFile.getParentFile(), triples.get("task")), triples.get("settings"),
+							triples.get("toolchain"), entry.getKey());
 				}
 			}
 		} catch (final FileNotFoundException e) {