Use proper YAML syntax for skip files

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

@@ -1,7 +1,17 @@
 # Timeout with Automizer, GemCutter succeeds
 TIMEOUT:
-- MirabelleConcurrentIncrement.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml
-- concurrent_increment.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml
-- equal-array-sums.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml
-- loop-lockstep-example.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml
-- sum_invariant.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml
+- task: MirabelleConcurrentIncrement.bpl
+  settings: ReachSafety-32bit-Automizer.epf
+  toolchain: ReachSafety.xml
+- task: concurrent_increment.bpl
+  settings: ReachSafety-32bit-Automizer.epf
+  toolchain: ReachSafety.xml
+- task: equal-array-sums.bpl
+  settings: ReachSafety-32bit-Automizer.epf
+  toolchain: ReachSafety.xml
+- task: loop-lockstep-example.bpl
+  settings: ReachSafety-32bit-Automizer.epf
+  toolchain: ReachSafety.xml
+- task: sum_invariant.bpl
+  settings: ReachSafety-32bit-Automizer.epf
+  toolchain: ReachSafety.xml

trunk/examples/concurrent/pthreads/races/regression/skip.yml

@@ -1,8 +1,16 @@
 TIMEOUT:
-- static-array-copy3.c DataRace-32bit-Automizer_Bitvector.epf DataRace.xml
-- static-array-copy3.c DataRace-32bit-Automizer_Default.epf DataRace.xml
-- static-array-copy3.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml
+- task: static-array-copy3.c
+  settings: DataRace-32bit-Automizer_Bitvector.epf
+  toolchain: DataRace.xml
+- task: static-array-copy3.c
+  settings: DataRace-32bit-Automizer_Default.epf
+  toolchain: DataRace.xml
+- task: static-array-copy3.c
+  settings: DataRace-32bit-GemCutter_Bitvector.epf
+  toolchain: DataRace.xml
 
 # Crash in MathSAT
 SMTLIBException.*mathsat:
-- struct-array-write.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml
+- task: struct-array-write.c
+  settings: DataRace-32bit-GemCutter_Bitvector.epf
+  toolchain: DataRace.xml

trunk/examples/concurrent/pthreads/regression/skip.yml

@@ -1,3 +1,5 @@
 # Timeout with Automizer, GemCutter succeeds
 TIMEOUT:
-- NonAtomicIncrement_2Threads.c ReachSafety-32bit-Automizer.epf ReachSafety.xml
+- task: NonAtomicIncrement_2Threads.c
+  settings: ReachSafety-32bit-Automizer.epf
+  toolchain: ReachSafety.xml

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

@@ -1,3 +1,7 @@
 TIMEOUT:
-- SAS09-Float.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml
-- ctrans-float-rounding.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml
+- task: SAS09-Float.c
+  settings: AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf
+  toolchain: AutomizerC.xml
+- task: ctrans-float-rounding.c
+  settings: AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf
+  toolchain: AutomizerC.xml

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

@@ -1,2 +1,4 @@
 overapproximation:
-- AuxVarInCall.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml
+- task: AuxVarInCall.bpl
+  settings: AutomizerBpl-forwardPredicates.epf
+  toolchain: AutomizerBpl.xml

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

@@ -1,21 +1,45 @@
 TIMEOUT:
-- BugLiveVariables03-Safe.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml
-- BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml
-- BugNoPredecessorOfReturnTransition.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml
-- nestedWhileSimple-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml
+- task: BugLiveVariables03-Safe.bpl
+  settings: AutomizerBpl-FPandBP.epf
+  toolchain: AutomizerBpl.xml
+- task: BugNestedSsaWithPendingContexts.bpl
+  settings: AutomizerBpl-forwardPredicates.epf
+  toolchain: AutomizerBpl.xml
+- task: BugNoPredecessorOfReturnTransition.bpl
+  settings: PdrAutomizerBpl.epf
+  toolchain: PdrAutomizerBpl.xml
+- task: nestedWhileSimple-Safe.bpl
+  settings: PdrAutomizerBpl.epf
+  toolchain: PdrAutomizerBpl.xml
 
 Overapproximation:
-- Overapproximation.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml
-- Overapproximation.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml
-- Overapproximation.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml
-- Overapproximation.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml
+- task: Overapproximation.bpl
+  settings: AutomizerBpl-nestedInterpolants.epf
+  toolchain: AutomizerBpl.xml
+- task: Overapproximation.bpl
+  settings: AutomizerBpl-forwardPredicates.epf
+  toolchain: AutomizerBpl.xml
+- task: Overapproximation.bpl
+  settings: AutomizerBpl-FPandBP.epf
+  toolchain: AutomizerBpl.xml
+- task: Overapproximation.bpl
+  settings: PdrAutomizerBpl.epf
+  toolchain: PdrAutomizerBpl.xml
 
 # We are unable to backtranslate @diff from SMT to Boogie
 unknown symbol (@diff:
-- BugLiveVariables03-Safe.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml
-- BugLiveVariables04-Safe.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml
+- task: BugLiveVariables03-Safe.bpl
+  settings: AutomizerBpl-nestedInterpolants.epf
+  toolchain: AutomizerBpl.xml
+- task: BugLiveVariables04-Safe.bpl
+  settings: AutomizerBpl-nestedInterpolants.epf
+  toolchain: AutomizerBpl.xml
 
 # Issue in SMTInterpol
 Const is only supported for infinite index sort:
-- ConstArray.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml
-- ConstArray.bpl AutomizerBpl-nestedInterpolants.epf PdrAutomizerBpl.xml
+- 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/skip.yml

@@ -1,49 +1,135 @@
 # Fails due to overapproximation of bitwise operators in the integer translation
 Overapproximation:
-- bitwiseOrUnsigned.c AutomizerC-forwardPredicates.epf AutomizerC.xml
-- bitwiseOrUnsigned.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml
-- bitwiseOrUnsigned.c AutomizerC-nestedInterpolants.epf AutomizerC.xml
-- bitwiseOrUnsigned.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml
-- bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml
-- bitwiseOrUnsigned.c KojakC-Reach-32Bit-Default.epf KojakC.xml
-- bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates.epf AutomizerC.xml
-- bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml
-- bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants.epf AutomizerC.xml
-- bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml
-- bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml
-- bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml
-- bitwiseOrUnsignedMinimal.c KojakC-Reach-32Bit-Default.epf KojakC.xml
-- builtin_ffs.c AutomizerC-forwardPredicates.epf AutomizerC.xml
-- builtin_ffs.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml
-- builtin_ffs.c AutomizerC-nestedInterpolants.epf AutomizerC.xml
-- builtin_ffs.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml
-- builtin_ffs.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml
-- builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml
-- builtin_ffs.c KojakC-Reach-32Bit-Default.epf KojakC.xml
-- BitwiseOperations02.c AutomizerC-forwardPredicates.epf AutomizerC.xml
-- BitwiseOperations02.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml
-- BitwiseOperations02.c AutomizerC-nestedInterpolants.epf AutomizerC.xml
-- BitwiseOperations02.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml
-- BitwiseOperations02.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml
-- BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.xml
+- task: bitwiseOrUnsigned.c
+  settings: AutomizerC-forwardPredicates.epf
+  toolchain: AutomizerC.xml
+- task: bitwiseOrUnsigned.c
+  settings: AutomizerC-forwardPredicates_const.epf
+  toolchain: AutomizerC.xml
+- task: bitwiseOrUnsigned.c
+  settings: AutomizerC-nestedInterpolants.epf
+  toolchain: AutomizerC.xml
+- task: bitwiseOrUnsigned.c
+  settings: AutomizerC-nestedInterpolants_const.epf
+  toolchain: AutomizerC.xml
+- task: bitwiseOrUnsigned.c
+  settings: BlockEncodingV2AutomizerC-forwardPredicates.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: bitwiseOrUnsigned.c
+  settings: KojakC-Reach-32Bit-Default.epf
+  toolchain: KojakC.xml
+- task: bitwiseOrUnsignedMinimal.c
+  settings: AutomizerC-forwardPredicates.epf
+  toolchain: AutomizerC.xml
+- task: bitwiseOrUnsignedMinimal.c
+  settings: AutomizerC-forwardPredicates_const.epf
+  toolchain: AutomizerC.xml
+- task: bitwiseOrUnsignedMinimal.c
+  settings: AutomizerC-nestedInterpolants.epf
+  toolchain: AutomizerC.xml
+- task: bitwiseOrUnsignedMinimal.c
+  settings: AutomizerC-nestedInterpolants_const.epf
+  toolchain: AutomizerC.xml
+- task: bitwiseOrUnsignedMinimal.c
+  settings: BlockEncodingV2AutomizerC-forwardPredicates.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: bitwiseOrUnsignedMinimal.c
+  settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: bitwiseOrUnsignedMinimal.c
+  settings: KojakC-Reach-32Bit-Default.epf
+  toolchain: KojakC.xml
+- task: builtin_ffs.c
+  settings: AutomizerC-forwardPredicates.epf
+  toolchain: AutomizerC.xml
+- task: builtin_ffs.c
+  settings: AutomizerC-forwardPredicates_const.epf
+  toolchain: AutomizerC.xml
+- task: builtin_ffs.c
+  settings: AutomizerC-nestedInterpolants.epf
+  toolchain: AutomizerC.xml
+- task: builtin_ffs.c
+  settings: AutomizerC-nestedInterpolants_const.epf
+  toolchain: AutomizerC.xml
+- task: builtin_ffs.c
+  settings: BlockEncodingV2AutomizerC-forwardPredicates.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: builtin_ffs.c
+  settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: builtin_ffs.c
+  settings: KojakC-Reach-32Bit-Default.epf
+  toolchain: KojakC.xml
+- task: BitwiseOperations02.c
+  settings: AutomizerC-forwardPredicates.epf
+  toolchain: AutomizerC.xml
+- task: BitwiseOperations02.c
+  settings: AutomizerC-forwardPredicates_const.epf
+  toolchain: AutomizerC.xml
+- task: BitwiseOperations02.c
+  settings: AutomizerC-nestedInterpolants.epf
+  toolchain: AutomizerC.xml
+- task: BitwiseOperations02.c
+  settings: AutomizerC-nestedInterpolants_const.epf
+  toolchain: AutomizerC.xml
+- task: BitwiseOperations02.c
+  settings: BlockEncodingV2AutomizerC-forwardPredicates.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: BitwiseOperations02.c
+  settings: KojakC-Reach-32Bit-Default.epf
+  toolchain: KojakC.xml
 
 TIMEOUT:
-- BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml
-- BitwiseOperations02.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml
-- ShortCircuit-SideEffect-DoStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml
-- ShortCircuit-SideEffect-ForStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml
-- StructPositiveSum-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml
-- StructPositiveSum-Safe.c AutomizerC-forwardPredicates.epf AutomizerC.xml
-- StructPositiveSum-Safe.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml
-- StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml
-- StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml
-- array10_pattern_simplified.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml
-- bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml
-- builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml
-- Acsl01-EnsuresLocal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml
-- Acsl03-EnsuresGlobal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml
-- Tschingelhorn-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml
+- task: BitwiseOperations01.c
+  settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: BitwiseOperations02.c
+  settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: ShortCircuit-SideEffect-DoStatement-Safe.c
+  settings: AutomizerC-BitvectorTranslation.epf
+  toolchain: AutomizerC.xml
+- task: ShortCircuit-SideEffect-ForStatement-Safe.c
+  settings: AutomizerC-BitvectorTranslation.epf
+  toolchain: AutomizerC.xml
+- task: StructPositiveSum-Safe.c
+  settings: AutomizerC-BitvectorTranslation.epf
+  toolchain: AutomizerC.xml
+- task: StructPositiveSum-Safe.c
+  settings: AutomizerC-forwardPredicates.epf
+  toolchain: AutomizerC.xml
+- task: StructPositiveSum-Safe.c
+  settings: AutomizerC-forwardPredicates_const.epf
+  toolchain: AutomizerC.xml
+- task: StructPositiveSum-Safe.c
+  settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: StructPositiveSum-Safe.c
+  settings: BlockEncodingV2AutomizerC-forwardPredicates.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- task: array10_pattern_simplified.c
+  settings: AutomizerC-BitvectorTranslation.epf
+  toolchain: AutomizerC.xml
+- task: bitwiseOrUnsigned.c
+  settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf
+  toolchain: BlockEncodingV2AutomizerC.xml
+- 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:
-- array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml
-- array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml
+- task: array10_pattern_simplified.c
+  settings: AutomizerC-nestedInterpolants.epf
+  toolchain: AutomizerC.xml
+- task: array10_pattern_simplified.c
+  settings: AutomizerC-nestedInterpolants_const.epf
+  toolchain: AutomizerC.xml

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

@@ -148,51 +148,17 @@ private static NestedMap3<String, String, String, String> getSkippedTests(final
 
 	private static void addSkippedTest(final File ignoreFile, final NestedMap3<String, String, String, String> map) {
 		try {
-			final Map<String, List<String>> parsed = new Yaml().load(new FileInputStream(ignoreFile));
+			final Map<String, List<Map<String, String>>> parsed = new Yaml().load(new FileInputStream(ignoreFile));
 			for (final var entry : parsed.entrySet()) {
-				for (final String line : entry.getValue()) {
-					addSkipLine(line, entry.getKey(), map);
+				for (final Map<String, String> triples : entry.getValue()) {
+					map.put(triples.get("task"), triples.get("settings"), triples.get("toolchain"), entry.getKey());
 				}
 			}
 		} catch (final FileNotFoundException e) {
 			// File does not exist, nothing to be ignored
 		}
 	}
 
-	private static void addSkipLine(final String line, final String exptectedVerdict,
-			final NestedMap3<String, String, String, String> map) {
-		if (line.startsWith("//")) {
-			return;
-		}
-		String settings = null;
-		String toolchain = null;
-		String file = null;
-		final String[] args = line.split("\\s+");
-		if (args.length != 3) {
-			return;
-		}
-		for (int i = 0; i < 3; i++) {
-			final String arg = args[i];
-			if (arg.endsWith(".epf")) {
-				if (settings != null) {
-					return;
-				}
-				settings = arg;
-			} else if (arg.endsWith(".xml")) {
-				if (toolchain != null) {
-					return;
-				}
-				toolchain = arg;
-			} else {
-				if (file != null) {
-					return;
-				}
-				file = arg;
-			}
-		}
-		map.put(file, settings, toolchain, exptectedVerdict);
-	}
-
 	protected long getTimeout(final Config rundef, final File file) {
 		return mTimeout;
 	}