Skip unsupported regression tests

trunk/examples/concurrent/bpl/regression/.testignore

@@ -0,0 +1,17 @@
+# Timeout with Automizer, GemCutter succeeds
+TIMEOUT:
+- 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/.testignore

@@ -0,0 +1,16 @@
+TIMEOUT:
+- 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:
+- task: struct-array-write.c
+  settings: DataRace-32bit-GemCutter_Bitvector.epf
+  toolchain: DataRace.xml

trunk/examples/concurrent/pthreads/regression/.testignore

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

trunk/examples/lassos/regression/.testignore

@@ -0,0 +1,5 @@
+# The program contains non-linear-arithmetic, so we don't succeed with the linear setting
+Unable to decide termination:
+- task: ConvincingNondeterminism01.bpl
+  settings: BuchiAutomizerBpl-linear.epf
+  toolchain: BuchiAutomizerBpl.xml

trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore

@@ -0,0 +1,7 @@
+TIMEOUT:
+- 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/.testignore

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

trunk/examples/programs/regression/bpl/.testignore

@@ -0,0 +1,4 @@
+TIMEOUT:
+- task: nestedWhileSimple-Safe.bpl
+  settings: PdrAutomizerBpl.epf
+  toolchain: PdrAutomizerBpl.xml

trunk/examples/programs/regression/bpl/interprocedural/.testignore

@@ -0,0 +1,19 @@
+TIMEOUT:
+- 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
+
+# We are unable to backtranslate @diff from SMT to Boogie
+unknown symbol.*@diff:
+- task: BugLiveVariables03-Safe.bpl
+  settings: AutomizerBpl-nestedInterpolants.epf
+  toolchain: AutomizerBpl.xml
+- task: BugLiveVariables04-Safe.bpl
+  settings: AutomizerBpl-nestedInterpolants.epf
+  toolchain: AutomizerBpl.xml

trunk/examples/programs/regression/bpl/toolDirectives/.testignore

@@ -0,0 +1,25 @@
+# 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
+- task: ConstArray.bpl
+  settings: PdrAutomizerBpl.epf
+  toolchain: PdrAutomizerBpl.xml
+
+Overapproximation:
+- 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

trunk/examples/programs/regression/c/.testignore

@@ -0,0 +1,126 @@
+# Fails due to overapproximation of bitwise operators in the integer translation
+Overapproximation:
+- 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:
+- 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
+
+unable to decide satisfiability of path constraint:
+- 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/examples/programs/regression/c/interprocedural/.testignore

@@ -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/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/UltimateTestCase.java

@@ -38,6 +38,7 @@
 import de.uni_freiburg.informatik.ultimate.test.decider.ITestResultDecider;
 import de.uni_freiburg.informatik.ultimate.test.decider.ITestResultDecider.TestResult;
 import de.uni_freiburg.informatik.ultimate.test.junitextension.testfactory.FactoryTestMethod;
+import de.uni_freiburg.informatik.ultimate.test.junitextension.testfactory.FactoryTestRunner.SkipTestException;
 import de.uni_freiburg.informatik.ultimate.test.mocks.ConsoleLogger;
 import de.uni_freiburg.informatik.ultimate.test.reporting.IIncrementalLog;
 import de.uni_freiburg.informatik.ultimate.test.reporting.ITestLogfile;
@@ -124,7 +125,7 @@ public void test() {
 			final ILogger logger = getLoggerFromStarter(starter);
 			logger.info("Deciding this test: " + deciderName);
 			result = mDecider.getTestResult(starter.getServices());
-			if (!returnCode.isOK() && result != TestResult.FAIL) {
+			if (!returnCode.isOK() && result != TestResult.FAIL && result != TestResult.IGNORE) {
 				logger.fatal("#################### Overwriting decision of " + deciderName
 						+ " and setting test status to FAIL ####################");
 				logger.fatal("Ultimate returned an unexpected status:");
@@ -183,7 +184,12 @@ public void test() {
 				}
 				if (th != null) {
 					message += " (Ultimate threw an Exception: " + th.getMessage() + ")";
+					if (result == TestResult.IGNORE) {
+						skipTest(message, th);
+					}
 					failTest(message, th);
+				} else if (result == TestResult.IGNORE) {
+					skipTest(message);
 				} else {
 					failTest(message);
 				}
@@ -266,6 +272,14 @@ private static void failTest(final String message, final Throwable th) throws Ul
 		throw exception;
 	}
 
+	private static void skipTest(final String message) {
+		throw new SkipTestException(message);
+	}
+
+	private static void skipTest(final String message, final Throwable cause) {
+		throw new SkipTestException(message, cause);
+	}
+
 	@Override
 	public int compareTo(final UltimateTestCase o) {
 		return mUltimateRunDefinition.compareTo(o.mUltimateRunDefinition);

trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ITestResultDecider.java

@@ -128,6 +128,10 @@ public enum TestResult {
 		/**
 		 * Success should always represent a JUnit test success.
 		 */
-		SUCCESS
+		SUCCESS,
+		/**
+		 * Marks a test as ignored
+		 */
+		IGNORE
 	}
 }

trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/SafetyCheckTestResultDecider.java

@@ -28,6 +28,8 @@
 
 package de.uni_freiburg.informatik.ultimate.test.decider;
 
+import java.util.regex.Pattern;
+
 import de.uni_freiburg.informatik.ultimate.core.lib.results.ExceptionOrErrorResult;
 import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition;
 import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.IExpectedResultFinder;
@@ -38,8 +40,7 @@
 import de.uni_freiburg.informatik.ultimate.test.util.TestUtil;
 
 /**
- * Use keywords in filename and first line to decide correctness of safety
- * checker results.
+ * Use keywords in filename and first line to decide correctness of safety checker results.
  *
  * @author [email protected]
  * @author Daniel Dietsch ([email protected])
@@ -50,19 +51,33 @@ public class SafetyCheckTestResultDecider extends ThreeTierTestResultDecider<Saf
 	/**
 	 *
 	 * @param ultimateRunDefinition
+	 * @param unknownIsJUnitSuccess
+	 *            if true the TestResult UNKNOWN is a success for JUnit, if false, the TestResult UNKNOWN is a failure
+	 *            for JUnit.
+	 *
+	 * @param overridenExpectedVerdict
+	 *            The expected verdict overridden in a separate file, null if not present.
+	 */
+	public SafetyCheckTestResultDecider(final UltimateRunDefinition ultimateRunDefinition,
+			final boolean unknownIsJUnitSuccess, final String overridenExpectedVerdict) {
+		super(ultimateRunDefinition, unknownIsJUnitSuccess, overridenExpectedVerdict);
+	}
+
+	/**
 	 *
+	 * @param ultimateRunDefinition
 	 * @param unknownIsJUnitSuccess
-	 *            if true the TestResult UNKNOWN is a success for JUnit, if
-	 *            false, the TestResult UNKNOWN is a failure for JUnit.
+	 *            if true the TestResult UNKNOWN is a success for JUnit, if false, the TestResult UNKNOWN is a failure
+	 *            for JUnit.
 	 */
-	public SafetyCheckTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, final boolean unknownIsJUnitSuccess) {
+	public SafetyCheckTestResultDecider(final UltimateRunDefinition ultimateRunDefinition,
+			final boolean unknownIsJUnitSuccess) {
 		super(ultimateRunDefinition, unknownIsJUnitSuccess);
 	}
 
 	@Override
 	public IExpectedResultFinder<SafetyCheckerOverallResult> constructExpectedResultFinder() {
-		return new KeywordBasedExpectedResultFinder<>(
-				TestUtil.constructFilenameKeywordMap_AllSafetyChecker(), null,
+		return new KeywordBasedExpectedResultFinder<>(TestUtil.constructFilenameKeywordMap_AllSafetyChecker(), null,
 				TestUtil.constructFirstlineKeywordMap_SafetyChecker());
 	}
 
@@ -84,6 +99,19 @@ public class SafetyCheckerTestResultEvaluation implements ITestResultEvaluation<
 		@Override
 		public void evaluateTestResult(final IExpectedResultFinder<SafetyCheckerOverallResult> expectedResultFinder,
 				final IOverallResultEvaluator<SafetyCheckerOverallResult> overallResultDeterminer) {
+			if (mOverridenExpectedVerdict != null) {
+				final SafetyCheckerOverallResult overallResult = overallResultDeterminer.getOverallResult();
+				final String overallResultMsg = overallResultDeterminer.generateOverallResultMessage();
+				final Pattern pattern = Pattern.compile(mOverridenExpectedVerdict, Pattern.CASE_INSENSITIVE);
+				if (pattern.matcher(overallResult.toString()) != null || pattern.matcher(overallResultMsg) != null) {
+					mTestResult = TestResult.IGNORE;
+				} else {
+					mTestResult = TestResult.FAIL;
+				}
+				mCategory = overallResult + " (Expected to match :" + mOverridenExpectedVerdict + ")";
+				mMessage = " UltimateResult: " + overallResultMsg;
+				return;
+			}
 			evaluateExpectedResult(expectedResultFinder);
 			switch (expectedResultFinder.getExpectedResultFinderStatus()) {
 			case ERROR: