diff --git a/trunk/examples/concurrent/bpl/regression/.testignore b/trunk/examples/concurrent/bpl/regression/.testignore new file mode 100644 index 00000000000..10b09b767bc --- /dev/null +++ b/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 diff --git a/trunk/examples/concurrent/pthreads/races/regression/.testignore b/trunk/examples/concurrent/pthreads/races/regression/.testignore new file mode 100644 index 00000000000..a5de3d6a4dd --- /dev/null +++ b/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 diff --git a/trunk/examples/concurrent/pthreads/regression/.testignore b/trunk/examples/concurrent/pthreads/regression/.testignore new file mode 100644 index 00000000000..f0fe6b28fd3 --- /dev/null +++ b/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 diff --git a/trunk/examples/lassos/regression/.testignore b/trunk/examples/lassos/regression/.testignore new file mode 100644 index 00000000000..a62b29f6d08 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore new file mode 100644 index 00000000000..98f261bbceb --- /dev/null +++ b/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 diff --git a/trunk/examples/programs/quantifier/regression/bpl/.testignore b/trunk/examples/programs/quantifier/regression/bpl/.testignore new file mode 100644 index 00000000000..425385046fb --- /dev/null +++ b/trunk/examples/programs/quantifier/regression/bpl/.testignore @@ -0,0 +1,4 @@ +overapproximation: +- task: AuxVarInCall.bpl + settings: AutomizerBpl-forwardPredicates.epf + toolchain: AutomizerBpl.xml diff --git a/trunk/examples/programs/regression/bpl/.testignore b/trunk/examples/programs/regression/bpl/.testignore new file mode 100644 index 00000000000..0e6d1d6de5b --- /dev/null +++ b/trunk/examples/programs/regression/bpl/.testignore @@ -0,0 +1,4 @@ +TIMEOUT: +- task: nestedWhileSimple-Safe.bpl + settings: PdrAutomizerBpl.epf + toolchain: PdrAutomizerBpl.xml diff --git a/trunk/examples/programs/regression/bpl/interprocedural/.testignore b/trunk/examples/programs/regression/bpl/interprocedural/.testignore new file mode 100644 index 00000000000..0680edba95a --- /dev/null +++ b/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 diff --git a/trunk/examples/programs/regression/bpl/toolDirectives/.testignore b/trunk/examples/programs/regression/bpl/toolDirectives/.testignore new file mode 100644 index 00000000000..ad375761f78 --- /dev/null +++ b/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 diff --git a/trunk/examples/programs/regression/c/.testignore b/trunk/examples/programs/regression/c/.testignore new file mode 100644 index 00000000000..9f91edc0a51 --- /dev/null +++ b/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 diff --git a/trunk/examples/programs/regression/c/interprocedural/.testignore b/trunk/examples/programs/regression/c/interprocedural/.testignore new file mode 100644 index 00000000000..623f87ba48e --- /dev/null +++ b/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 diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/UltimateTestCase.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/UltimateTestCase.java index f5e6e7ce22a..0effe6b2aa3 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/UltimateTestCase.java +++ b/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); diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ITestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ITestResultDecider.java index a564bc40151..e129c9f14b9 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ITestResultDecider.java +++ b/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 } } diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/SafetyCheckTestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/SafetyCheckTestResultDecider.java index f6245a295cb..1bcfa093b33 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/SafetyCheckTestResultDecider.java +++ b/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 heizmann@informatik.uni-freiburg.de * @author Daniel Dietsch (dietsch@informatik.uni-freiburg.de) @@ -50,19 +51,33 @@ public class SafetyCheckTestResultDecider extends ThreeTierTestResultDecider 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 expectedResultFinder, final IOverallResultEvaluator 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: diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/TerminationAnalysisTestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/TerminationAnalysisTestResultDecider.java index be758501fe6..e76b822d0a1 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/TerminationAnalysisTestResultDecider.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/TerminationAnalysisTestResultDecider.java @@ -26,6 +26,8 @@ */ package de.uni_freiburg.informatik.ultimate.test.decider; +import java.util.regex.Pattern; + import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition; import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.IExpectedResultFinder; import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.KeywordBasedExpectedResultFinder; @@ -50,6 +52,11 @@ public TerminationAnalysisTestResultDecider( super(ultimateRunDefinition, unknownIsJUnitSuccess); } + public TerminationAnalysisTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, + final boolean unknownIsJUnitSuccess, final String overridenExpectedVerdict) { + super(ultimateRunDefinition, unknownIsJUnitSuccess, overridenExpectedVerdict); + } + @Override public IExpectedResultFinder constructExpectedResultFinder() { return new KeywordBasedExpectedResultFinder<>( @@ -79,6 +86,19 @@ public class TerminationAnalysisResultEvaluation implements ITestResultEvaluatio public void evaluateTestResult( final IExpectedResultFinder expectedResultFinder, final IOverallResultEvaluator overallResultDeterminer) { + if (mOverridenExpectedVerdict != null) { + final TerminationAnalysisOverallResult 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: diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ThreeTierTestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ThreeTierTestResultDecider.java index a57530f01c4..e8770e5b78e 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ThreeTierTestResultDecider.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ThreeTierTestResultDecider.java @@ -59,6 +59,7 @@ public abstract class ThreeTierTestResultDecider implements ITes private final IExpectedResultFinder mExpectedResultEvaluation; private IOverallResultEvaluator mUltimateResultEvaluation; private ITestResultEvaluation mTestResultEvaluation; + protected final String mOverridenExpectedVerdict; /** * @@ -67,15 +68,32 @@ public abstract class ThreeTierTestResultDecider implements ITes * @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 ThreeTierTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, - final boolean unknownIsJUnitSuccess) { + final boolean unknownIsJUnitSuccess, final String overridenExpectedVerdict) { mUnknownIsJUnitSuccess = unknownIsJUnitSuccess; + mOverridenExpectedVerdict = overridenExpectedVerdict; mUltimateRunDefinition = ultimateRunDefinition; mExpectedResultEvaluation = constructExpectedResultFinder(); mExpectedResultEvaluation.findExpectedResult(ultimateRunDefinition); } + /** + * + * @param ultimateRunDefinition + * + * @param unknownIsJUnitSuccess + * if true the TestResult UNKNOWN is a success for JUnit, if false, the TestResult UNKNOWN is a failure + * for JUnit. + */ + public ThreeTierTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, + final boolean unknownIsJUnitSuccess) { + this(ultimateRunDefinition, unknownIsJUnitSuccess, null); + } + @Override public final TestResult getTestResult(final IUltimateServiceProvider services) { mUltimateResultEvaluation = constructUltimateResultEvaluation(); @@ -123,8 +141,10 @@ public boolean getJUnitSuccess(final TestResult testResult) { return mUnknownIsJUnitSuccess; case FAIL: return false; + case IGNORE: + return false; default: - throw new AssertionError("unknown actualResult"); + throw new AssertionError("unknown actualResult: " + testResult); } } diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/junitextension/testfactory/FactoryTestRunner.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/junitextension/testfactory/FactoryTestRunner.java index a8deda4a9b8..366949f2963 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/junitextension/testfactory/FactoryTestRunner.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/junitextension/testfactory/FactoryTestRunner.java @@ -47,7 +47,11 @@ import java.util.stream.Collector; import org.junit.AfterClass; +import org.junit.internal.AssumptionViolatedException; import org.junit.internal.runners.statements.RunAfters; +import org.junit.runner.Description; +import org.junit.runner.notification.Failure; +import org.junit.runner.notification.RunNotifier; import org.junit.runners.BlockJUnit4ClassRunner; import org.junit.runners.model.FrameworkMethod; import org.junit.runners.model.InitializationError; @@ -186,6 +190,54 @@ protected List computeTestMethods() { return mTests; } + @Override + protected void runChild(final FrameworkMethod method, final RunNotifier notifier) { + final Description description = describeChild(method); + if (isIgnored(method)) { + notifier.fireTestIgnored(description); + } else { + final Statement statement = new Statement() { + @Override + public void evaluate() throws Throwable { + methodBlock(method).evaluate(); + } + }; + myRunLeaf(method, description, notifier); + } + } + + protected final void myRunLeaf(final FrameworkMethod method, final Description description, + final RunNotifier notifier) { + notifier.fireTestStarted(description); + try { + methodBlock(method).evaluate(); + } catch (final AssumptionViolatedException e) { + notifier.fireTestAssumptionFailed(new Failure(description, e)); + } catch (final SkipTestException e) { + notifier.fireTestIgnored(description); + } catch (final Throwable e) { + notifier.fireTestFailure(new Failure(description, e)); + } finally { + notifier.fireTestFinished(description); + } + } + + public static class SkipTestException extends RuntimeException { + private static final long serialVersionUID = 1L; + + public SkipTestException() { + super(); + } + + public SkipTestException(final String message) { + super(message); + } + + public SkipTestException(final String message, final Throwable cause) { + super(message, cause); + } + } + @Override protected Object createTest() throws Exception { return mTestSuiteInstance; diff --git a/trunk/source/UltimateRegressionTest/META-INF/MANIFEST.MF b/trunk/source/UltimateRegressionTest/META-INF/MANIFEST.MF index b1d74518ecf..5094b7578c9 100644 --- a/trunk/source/UltimateRegressionTest/META-INF/MANIFEST.MF +++ b/trunk/source/UltimateRegressionTest/META-INF/MANIFEST.MF @@ -30,7 +30,8 @@ Require-Bundle: org.junit, de.uni_freiburg.informatik.ultimate.plugins.icfgtransformation, de.uni_freiburg.informatik.ultimate.lib.sifa, de.uni_freiburg.informatik.ultimate.plugins.sifa, - de.uni_freiburg.informatik.ultimate.plugins.generator.referee + de.uni_freiburg.informatik.ultimate.plugins.generator.referee, + org.yaml.snakeyaml Import-Package: de.uni_freiburg.informatik.ultimate.lib.pea, de.uni_freiburg.informatik.ultimate.lib.srparse, de.uni_freiburg.informatik.ultimate.lib.srparse.pattern, diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java index ef465d8905c..4ac5d6092bf 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java @@ -27,17 +27,22 @@ package de.uni_freiburg.informatik.ultimate.regressiontest; import java.io.File; +import java.io.FileInputStream; +import java.io.FileNotFoundException; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; import java.util.Collections; import java.util.HashSet; import java.util.List; +import java.util.Map; import java.util.Set; import java.util.function.Predicate; import java.util.regex.Matcher; import java.util.stream.Collectors; +import org.yaml.snakeyaml.Yaml; + import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition; import de.uni_freiburg.informatik.ultimate.test.UltimateTestCase; import de.uni_freiburg.informatik.ultimate.test.UltimateTestSuite; @@ -48,6 +53,7 @@ import de.uni_freiburg.informatik.ultimate.test.reporting.IIncrementalLog; import de.uni_freiburg.informatik.ultimate.test.reporting.ITestSummary; import de.uni_freiburg.informatik.ultimate.test.util.TestUtil; +import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.NestedMap3; /** * An {@link AbstractRegressionTestSuite} is a {@link UltimateTestSuite} that automatically generates tests from folders @@ -62,6 +68,7 @@ public abstract class AbstractRegressionTestSuite extends UltimateTestSuite { private static final Predicate FILTER_XML = TestUtil.getFileEndingTest(".xml"); private static final Predicate FILTER_EPF = TestUtil.getFileEndingTest(".epf"); + private static final String SKIPPED_FILENAME = ".testignore"; protected long mTimeout; protected String mRootFolder; @@ -110,17 +117,51 @@ public Collection createTestCases() { final Predicate filesRegexFilter = getFilesRegexFilter(); for (final Config runConfiguration : runConfigurations) { final Collection inputFiles = getInputFiles(filesRegexFilter, runConfiguration); - + final NestedMap3 skippedTests = getSkippedTests(inputFiles); for (final File inputFile : inputFiles) { final UltimateRunDefinition urd = new UltimateRunDefinition(inputFile, runConfiguration.getSettingsFile(), runConfiguration.getToolchainFile(), getTimeout(runConfiguration, inputFile)); - rtr.add(buildTestCase(urd, getTestResultDecider(urd))); + final String overridenVerdict = skippedTests.get(inputFile, + runConfiguration.getSettingsFile().getName(), runConfiguration.getToolchainFile().getName()); + final ITestResultDecider decider = overridenVerdict == null ? getTestResultDecider(urd) + : getTestResultDecider(urd, overridenVerdict); + rtr.add(buildTestCase(urd, decider)); } } return rtr; } + /** + * 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 getSkippedTests(final Collection inputFiles) { + final NestedMap3 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 map) { + try { + final Map>> parsed = new Yaml().load(new FileInputStream(ignoreFile)); + for (final var entry : parsed.entrySet()) { + for (final Map triples : entry.getValue()) { + 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) { + // File does not exist, nothing to be ignored + } + } + protected long getTimeout(final Config rundef, final File file) { return mTimeout; } @@ -266,6 +307,11 @@ protected Collection getInputFiles(final Predicate regexFilter, fina protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + 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 { diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java index 9911bef4a16..afee2f0b027 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java @@ -51,14 +51,14 @@ public ChcRegressionTestSuite() { mTimeout = DEFAULT_TIMEOUT; mRootFolder = TestUtil.getPathFromTrunk("examples/smtlib/horn/regression"); -// // exclude paths that match the following regex -// mExcludeFilterRegex = + // // exclude paths that match the following regex + // mExcludeFilterRegex = mFiletypesToConsider = new String[] { ".smt2" }; } @Override protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { - boolean unknownIsSuccess = false; + final boolean unknownIsSuccess = false; return new ChcTestResultDecider(runDefinition, unknownIsSuccess); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java index 29547da85ac..9ee56f54f3f 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java @@ -26,16 +26,11 @@ */ package de.uni_freiburg.informatik.ultimate.regressiontest.generic; -import java.io.File; -import java.util.HashMap; -import java.util.Map; - import de.uni_freiburg.informatik.ultimate.regressiontest.AbstractRegressionTestSuite; import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition; import de.uni_freiburg.informatik.ultimate.test.decider.ITestResultDecider; import de.uni_freiburg.informatik.ultimate.test.decider.SafetyCheckTestResultDecider; import de.uni_freiburg.informatik.ultimate.test.util.TestUtil; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; public class DataRaceRegressionTestSuite extends AbstractRegressionTestSuite { @@ -43,16 +38,11 @@ public class DataRaceRegressionTestSuite extends AbstractRegressionTestSuite { private static final String ROOT_DIR = TestUtil.getPathFromTrunk("examples/concurrent/pthreads/races"); private static final String FILE_ENDING = ".c"; - private final Map, Long> mSpecialTimeouts = new HashMap<>(); - public DataRaceRegressionTestSuite() { super(); mTimeout = TIMEOUT; mRootFolder = ROOT_DIR; mFiletypesToConsider = new String[] { FILE_ENDING }; - - mSpecialTimeouts.put(new Pair<>("DataRace-32bit-Automizer_Bitvector.epf", "static-array-copy3.c"), 250_000L); - mSpecialTimeouts.put(new Pair<>("DataRace-32bit-Automizer_Default.epf", "static-array-copy3.c"), 40_000L); } @Override @@ -61,12 +51,8 @@ protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition ru } @Override - protected long getTimeout(final Config config, final File file) { - final var pair = new Pair<>(config.getSettingsFile().getName(), file.getName()); - final var timeout = mSpecialTimeouts.get(pair); - if (timeout != null) { - return timeout; - } - return super.getTimeout(config, file); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + return new SafetyCheckTestResultDecider(runDefinition, false, overridenExpectedVerdict); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/RegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/RegressionTestSuite.java index 0bcea8519e7..e8609420382 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/RegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/RegressionTestSuite.java @@ -58,4 +58,10 @@ protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition ru return new SafetyCheckTestResultDecider(runDefinition, false); } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + return new SafetyCheckTestResultDecider(runDefinition, false, overridenExpectedVerdict); + } + } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java index d2026acec37..0613dd93d1b 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java @@ -173,7 +173,8 @@ public boolean isSuccess(final ReqCheckerResult actual) { } return false; } - if ((mNoResults != -1 && actual.mNoResults != mNoResults) || DataStructureUtils.isDifferent(actual.mRedundant, mRedundant)) { + if ((mNoResults != -1 && actual.mNoResults != mNoResults) + || DataStructureUtils.isDifferent(actual.mRedundant, mRedundant)) { return false; } return true; diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/SignedIntegerOverflowRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/SignedIntegerOverflowRegressionTestSuite.java index d63f434fd8b..8dadef23f02 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/SignedIntegerOverflowRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/SignedIntegerOverflowRegressionTestSuite.java @@ -52,4 +52,10 @@ protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition ru return new SafetyCheckTestResultDecider(runDefinition, false); } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + return new SafetyCheckTestResultDecider(runDefinition, false, overridenExpectedVerdict); + } + } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java index 7464ca629cf..8d7d383a8b2 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java @@ -54,4 +54,10 @@ protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition ru return new TerminationAnalysisTestResultDecider(runDefinition, false); } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + return new TerminationAnalysisTestResultDecider(runDefinition, false, overridenExpectedVerdict); + } + }