From 8b4ea8ffee344657397acc21c44f54f9efe1e36c Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Mon, 19 Dec 2022 18:42:39 +0100 Subject: [PATCH 01/42] add support for ignoring tests after running them --- .../testfactory/FactoryTestRunner.java | 52 +++++++++++++++++++ 1 file changed, 52 insertions(+) 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; From 12536f93c6438d182281da6c1159574f35b06507 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Mon, 19 Dec 2022 18:44:02 +0100 Subject: [PATCH 02/42] preliminary support for test result deciders to skip tests --- .../informatik/ultimate/test/UltimateTestCase.java | 14 ++++++++++++++ .../ultimate/test/decider/ITestResultDecider.java | 6 +++++- .../test/decider/ThreeTierTestResultDecider.java | 4 +++- 3 files changed, 22 insertions(+), 2 deletions(-) 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..1a101b73deb 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; @@ -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/ThreeTierTestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ThreeTierTestResultDecider.java index a57530f01c4..59e05e4f32e 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 @@ -123,8 +123,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); } } From f3ad4f92293536e4e5b064a7aada39e26be9604c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Fri, 10 Feb 2023 16:55:25 +0100 Subject: [PATCH 03/42] First attempt to check if a test case is ignored --- .../AbstractRegressionTestSuite.java | 32 ++++++++++++++++--- ...gieBacktranslationRegressionTestSuite.java | 2 +- .../CBacktranslationRegressionTestSuite.java | 2 +- .../generic/AbsIntRegressionTestSuite.java | 2 +- .../AutomataLibraryRegressionTestSuite.java | 2 +- .../generic/ChcRegressionTestSuite.java | 2 +- .../generic/DataRaceRegressionTestSuite.java | 2 +- .../generic/LTLRegressionTestSuite.java | 2 +- .../generic/MSODRegressionTestSuite.java | 2 +- .../generic/RegressionTestSuite.java | 2 +- .../ReqCheckerRegressionTestSuite.java | 2 +- ...nedIntegerOverflowRegressionTestSuite.java | 2 +- .../TerminationRegressionTestSuite.java | 2 +- .../C2BoogieRegressionTestSuite.java | 2 +- .../LTLTranslationRegressionTestSuite.java | 2 +- 15 files changed, 42 insertions(+), 18 deletions(-) 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..db37280d74b 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 @@ -26,7 +26,11 @@ */ package de.uni_freiburg.informatik.ultimate.regressiontest; +import java.io.BufferedReader; import java.io.File; +import java.io.FileInputStream; +import java.io.IOException; +import java.io.InputStreamReader; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; @@ -48,6 +52,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.Triple; /** * An {@link AbstractRegressionTestSuite} is a {@link UltimateTestSuite} that automatically generates tests from folders @@ -110,17 +115,36 @@ public Collection createTestCases() { final Predicate filesRegexFilter = getFilesRegexFilter(); for (final Config runConfiguration : runConfigurations) { final Collection inputFiles = getInputFiles(filesRegexFilter, runConfiguration); - + // TODO: Better path + final Set> ignoredTestFails = + getIgnoredTestFails(new File(runConfiguration.getSettingsFile().getParentFile(), "ignored.txt")); 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 boolean isIgnored = ignoredTestFails.contains(new Triple<>(inputFile.getName(), + runConfiguration.getSettingsFile().getName(), runConfiguration.getToolchainFile().getName())); + rtr.add(buildTestCase(urd, getTestResultDecider(urd, isIgnored))); } } return rtr; } + private static Set> getIgnoredTestFails(final File ignoreFile) { + final Set> ignoredTestFails = new HashSet<>(); + try (BufferedReader br = new BufferedReader(new InputStreamReader(new FileInputStream(ignoreFile)))) { + String line; + while ((line = br.readLine()) != null) { + final String[] args = line.split("\\s+"); + assert args.length == 3; + ignoredTestFails.add(new Triple<>(args[0], args[1], args[2])); + } + } catch (final IOException e) { + // Just skip + } + return ignoredTestFails; + } + protected long getTimeout(final Config rundef, final File file) { return mTimeout; } @@ -264,10 +288,10 @@ protected Collection getInputFiles(final Predicate regexFilter, fina .collect(Collectors.toList()); } - protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition); + protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition, boolean isIgnored); public static final class Config - extends de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair { + extends de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair { public Config(final File toolchain, final File settings) { super(toolchain, settings); diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java index 8b718651698..6b958902198 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java @@ -46,7 +46,7 @@ public BoogieBacktranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new BacktranslationTestResultDecider(runDefinition); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java index 26d4db005c7..ccba31b164a 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java @@ -46,7 +46,7 @@ public CBacktranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new BacktranslationTestResultDecider(runDefinition); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java index fb6bf240826..24abd35bbd1 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java @@ -51,7 +51,7 @@ public AbsIntRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new OverapproximatingSafetyCheckTestResultDecider(runDefinition, true); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java index c167bca53d5..c17116f91b6 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java @@ -50,7 +50,7 @@ public AutomataLibraryRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new AutomataScriptTestResultDecider(); } 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..c9fd2b9e739 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 @@ -57,7 +57,7 @@ public ChcRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { 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..b35bc7f8a48 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 @@ -56,7 +56,7 @@ public DataRaceRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new SafetyCheckTestResultDecider(runDefinition, false); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java index 2bae9b85ab4..3c316d72e5c 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java @@ -49,7 +49,7 @@ public LTLRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new LTLCheckerTestResultDecider(runDefinition, false); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java index 5118211951d..67f47fc8341 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java @@ -51,7 +51,7 @@ public MSODRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { final boolean unknownIsSuccess = true; return new MSODTestResultDecider(runDefinition, unknownIsSuccess); } 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..ab966c09a72 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 @@ -54,7 +54,7 @@ public RegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new SafetyCheckTestResultDecider(runDefinition, false); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java index 7c74c33fcab..73fb831f66b 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java @@ -79,7 +79,7 @@ public ReqCheckerRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new ReqCheckerTestResultDecider(runDefinition, false); } 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..55b75e55912 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 @@ -48,7 +48,7 @@ public SignedIntegerOverflowRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new SafetyCheckTestResultDecider(runDefinition, false); } 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..c4b3a9260ed 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 @@ -50,7 +50,7 @@ public TerminationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new TerminationAnalysisTestResultDecider(runDefinition, false); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java index e1eafac9941..53c0b245d09 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java @@ -66,7 +66,7 @@ public C2BoogieRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new TranslationTestResultDecider(runDefinition.selectPrimaryInputFile()); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java index 4ae4a304130..28d0d5314fd 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java @@ -48,7 +48,7 @@ public LTLTranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { return new TranslationTestResultDecider(runDefinition.selectPrimaryInputFile()); } From 8fae4cddc8fd812c3e6257cd09c554abba41fb1e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Fri, 10 Feb 2023 17:10:06 +0100 Subject: [PATCH 04/42] Add possibility to ignore test failures to SafetyCheckTestResultDecider --- .../decider/SafetyCheckTestResultDecider.java | 36 +++++++++++++------ .../decider/ThreeTierTestResultDecider.java | 20 ++++++++++- .../generic/RegressionTestSuite.java | 4 +-- 3 files changed, 46 insertions(+), 14 deletions(-) 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..5d2b2b39a63 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 @@ -38,8 +38,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 +49,30 @@ public class SafetyCheckTestResultDecider extends ThreeTierTestResultDecider constructExpectedResultFinder() { - return new KeywordBasedExpectedResultFinder<>( - TestUtil.constructFilenameKeywordMap_AllSafetyChecker(), null, + return new KeywordBasedExpectedResultFinder<>(TestUtil.constructFilenameKeywordMap_AllSafetyChecker(), null, TestUtil.constructFirstlineKeywordMap_SafetyChecker()); } @@ -107,6 +117,10 @@ private void evaluateOverallResultWithoutExpectedResult( mCategory = overallResult + " (Expected:UNKNOWN)"; mMessage += " UltimateResult: " + overallResultMsg; + if (mIsIgnored) { + mTestResult = TestResult.IGNORE; + return; + } switch (overallResult) { case EXCEPTION_OR_ERROR: case UNSUPPORTED_SYNTAX: @@ -139,7 +153,7 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes switch (overallResult) { case EXCEPTION_OR_ERROR: mCategory = overallResult + " (Expected:" + expectedResult + ") " + overallResultMsg; - mTestResult = TestResult.FAIL; + mTestResult = mIsIgnored ? TestResult.IGNORE : TestResult.FAIL; break; case SAFE: if (expectedResult == SafetyCheckerOverallResult.SAFE) { @@ -166,7 +180,7 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes } else if (expectedResult == SafetyCheckerOverallResult.UNSAFE) { mTestResult = TestResult.SUCCESS; } else { - mTestResult = TestResult.UNKNOWN; + mTestResult = mIsIgnored ? TestResult.IGNORE : TestResult.UNKNOWN; } break; case INVALID_ANNOTATION: @@ -182,7 +196,7 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes if (expectedResult == SafetyCheckerOverallResult.SYNTAX_ERROR) { mTestResult = TestResult.FAIL; } else { - mTestResult = TestResult.UNKNOWN; + mTestResult = mIsIgnored ? TestResult.IGNORE : TestResult.UNKNOWN; } break; case SYNTAX_ERROR: @@ -197,7 +211,7 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes if (expectedResult == SafetyCheckerOverallResult.SYNTAX_ERROR) { mTestResult = TestResult.FAIL; } else { - mTestResult = TestResult.UNKNOWN; + mTestResult = mIsIgnored ? TestResult.IGNORE : TestResult.UNKNOWN; } break; case UNSUPPORTED_SYNTAX: 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 59e05e4f32e..443e06ef4e7 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 boolean mIsIgnored; /** * @@ -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 isIgnored + * Is the test case ignored? */ public ThreeTierTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, - final boolean unknownIsJUnitSuccess) { + final boolean unknownIsJUnitSuccess, final boolean isIgnored) { mUnknownIsJUnitSuccess = unknownIsJUnitSuccess; + mIsIgnored = isIgnored; 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, false); + } + @Override public final TestResult getTestResult(final IUltimateServiceProvider services) { mUltimateResultEvaluation = constructUltimateResultEvaluation(); 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 ab966c09a72..3a72b11c26a 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 @@ -54,8 +54,8 @@ public RegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { - return new SafetyCheckTestResultDecider(runDefinition, false); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final boolean isIgnored) { + return new SafetyCheckTestResultDecider(runDefinition, false, isIgnored); } } From a03eee87e20dc36ec22434655856ac6361837698 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Fri, 10 Feb 2023 18:07:23 +0100 Subject: [PATCH 05/42] Don't overwrite IGNORE result --- .../uni_freiburg/informatik/ultimate/test/UltimateTestCase.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 1a101b73deb..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 @@ -125,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:"); From 2547848bad177de24b99056402460bdb990618ef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Fri, 10 Feb 2023 18:09:56 +0100 Subject: [PATCH 06/42] Skip overflow tests as well --- .../generic/SignedIntegerOverflowRegressionTestSuite.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 55b75e55912..d49cb4fd1be 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 @@ -48,8 +48,8 @@ public SignedIntegerOverflowRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { - return new SafetyCheckTestResultDecider(runDefinition, false); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final boolean isIgnored) { + return new SafetyCheckTestResultDecider(runDefinition, false, isIgnored); } } From 8cbef8194a895cfb908dacaad7f675a3bdd216ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Fri, 10 Feb 2023 18:27:50 +0100 Subject: [PATCH 07/42] Ignore safety tests in various folders --- .../concurrent/bpl/regression/ignored.txt | 6 ++++++ .../FloatingPoint/regression/c/ignored.txt | 4 ++++ .../regression/ignored.txt | 2 ++ .../regression/bpl/interprocedural/ignored.txt | 2 ++ .../examples/programs/regression/c/ignored.txt | 18 ++++++++++++++++++ 5 files changed, 32 insertions(+) create mode 100644 trunk/examples/concurrent/bpl/regression/ignored.txt create mode 100644 trunk/examples/programs/FloatingPoint/regression/c/ignored.txt create mode 100644 trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt create mode 100644 trunk/examples/programs/regression/bpl/interprocedural/ignored.txt create mode 100644 trunk/examples/programs/regression/c/ignored.txt diff --git a/trunk/examples/concurrent/bpl/regression/ignored.txt b/trunk/examples/concurrent/bpl/regression/ignored.txt new file mode 100644 index 00000000000..5d7cd7d8cb2 --- /dev/null +++ b/trunk/examples/concurrent/bpl/regression/ignored.txt @@ -0,0 +1,6 @@ +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 +NonAtomicIncrement_2Threads.c ReachSafety-32bit-Automizer.epf ReachSafety.xml diff --git a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt new file mode 100644 index 00000000000..05beca73fca --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt @@ -0,0 +1,4 @@ +BvaddWithThreeArguments.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +SAS09-Float.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml +SAS09-Float.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +cbmc_float4_PART1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml diff --git a/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt b/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt new file mode 100644 index 00000000000..6cce0268f0b --- /dev/null +++ b/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt @@ -0,0 +1,2 @@ +ShiftLeft06.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml +ShiftLeft07.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml diff --git a/trunk/examples/programs/regression/bpl/interprocedural/ignored.txt b/trunk/examples/programs/regression/bpl/interprocedural/ignored.txt new file mode 100644 index 00000000000..2b551248ee6 --- /dev/null +++ b/trunk/examples/programs/regression/bpl/interprocedural/ignored.txt @@ -0,0 +1,2 @@ +BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml +BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml diff --git a/trunk/examples/programs/regression/c/ignored.txt b/trunk/examples/programs/regression/c/ignored.txt new file mode 100644 index 00000000000..33479e2ba85 --- /dev/null +++ b/trunk/examples/programs/regression/c/ignored.txt @@ -0,0 +1,18 @@ +BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.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-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml +BitwiseOperations02.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml +BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.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 +array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml +array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml From 688f032029cabd15a055514d0f56944f429b09f2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Mon, 13 Feb 2023 13:56:44 +0100 Subject: [PATCH 08/42] Ignore some more tests and move to the correct location --- .../concurrent/pthreads/regression/ignored.txt | 1 + .../programs/FloatingPoint/regression/c/ignored.txt | 10 ++++++++++ trunk/examples/programs/regression/bpl/ignored.txt | 5 +++++ .../regression/bpl/interprocedural/ignored.txt | 2 -- 4 files changed, 16 insertions(+), 2 deletions(-) create mode 100644 trunk/examples/concurrent/pthreads/regression/ignored.txt create mode 100644 trunk/examples/programs/regression/bpl/ignored.txt delete mode 100644 trunk/examples/programs/regression/bpl/interprocedural/ignored.txt diff --git a/trunk/examples/concurrent/pthreads/regression/ignored.txt b/trunk/examples/concurrent/pthreads/regression/ignored.txt new file mode 100644 index 00000000000..d6ab96ff834 --- /dev/null +++ b/trunk/examples/concurrent/pthreads/regression/ignored.txt @@ -0,0 +1 @@ +NonAtomicIncrement_2Threads.c ReachSafety-32bit-Automizer.epf ReachSafety.xml diff --git a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt index 05beca73fca..6853ffa4931 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt +++ b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt @@ -2,3 +2,13 @@ BvaddWithThreeArguments.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Cons SAS09-Float.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml SAS09-Float.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml cbmc_float4_PART1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +ctrans-float-rounding.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml +ctrans-float-rounding.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +cbmc_float-no-simp1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +cbmc_float-to-double2.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +cbmc_float12.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +cbmc_float13.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +cbmc_float19.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +cbmc_float20_Part1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +cbmc_float20_Part3.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +cbmc_float6.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml diff --git a/trunk/examples/programs/regression/bpl/ignored.txt b/trunk/examples/programs/regression/bpl/ignored.txt new file mode 100644 index 00000000000..38341c3da68 --- /dev/null +++ b/trunk/examples/programs/regression/bpl/ignored.txt @@ -0,0 +1,5 @@ +BugLiveVariables03-Safe.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml +BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml +BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml +BugNoPredecessorOfReturnTransition.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml +nestedWhileSimple-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml diff --git a/trunk/examples/programs/regression/bpl/interprocedural/ignored.txt b/trunk/examples/programs/regression/bpl/interprocedural/ignored.txt deleted file mode 100644 index 2b551248ee6..00000000000 --- a/trunk/examples/programs/regression/bpl/interprocedural/ignored.txt +++ /dev/null @@ -1,2 +0,0 @@ -BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml -BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml From da2b1a019408c652dc8849a0632a0f1b2414fea2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Wed, 15 Feb 2023 14:51:41 +0100 Subject: [PATCH 09/42] Ignore another test --- trunk/examples/programs/FloatingPoint/regression/c/ignored.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt index 6853ffa4931..a4993acc42b 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt +++ b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt @@ -12,3 +12,4 @@ cbmc_float19.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf Autom cbmc_float20_Part1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml cbmc_float20_Part3.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml cbmc_float6.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +QuantifiedFloatInvariant.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml From 1f787f0a1f82c6467aed3d4f1bcb795e6188856c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Wed, 15 Feb 2023 15:09:59 +0100 Subject: [PATCH 10/42] Improve parsing of ignore file --- .../AbstractRegressionTestSuite.java | 43 ++++++++++++++++--- 1 file changed, 38 insertions(+), 5 deletions(-) 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 db37280d74b..4a51d39f16a 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 @@ -130,14 +130,15 @@ public Collection createTestCases() { return rtr; } - private static Set> getIgnoredTestFails(final File ignoreFile) { + private static Set> getIgnoredTestFails(final File ignoreFile) { final Set> ignoredTestFails = new HashSet<>(); try (BufferedReader br = new BufferedReader(new InputStreamReader(new FileInputStream(ignoreFile)))) { String line; while ((line = br.readLine()) != null) { - final String[] args = line.split("\\s+"); - assert args.length == 3; - ignoredTestFails.add(new Triple<>(args[0], args[1], args[2])); + final Triple triple = parseIgnoreLine(line); + if (triple != null) { + ignoredTestFails.add(triple); + } } } catch (final IOException e) { // Just skip @@ -145,6 +146,38 @@ private static Set> getIgnoredTestFails(final Fi return ignoredTestFails; } + private static Triple parseIgnoreLine(final String line) { + if (line.startsWith("//")) { + return null; + } + String settings = null; + String toolchain = null; + String file = null; + final String[] args = line.split("\\s+"); + if (args.length != 3) { + return null; + } + for (final String arg : args) { + if (arg.endsWith(".epf")) { + if (settings != null) { + return null; + } + settings = arg; + } else if (arg.endsWith(".xml")) { + if (toolchain != null) { + return null; + } + toolchain = arg; + } else { + if (file != null) { + return null; + } + file = arg; + } + } + return new Triple<>(file, settings, toolchain); + } + protected long getTimeout(final Config rundef, final File file) { return mTimeout; } @@ -291,7 +324,7 @@ protected Collection getInputFiles(final Predicate regexFilter, fina protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition, boolean isIgnored); public static final class Config - extends de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair { + extends de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair { public Config(final File toolchain, final File settings) { super(toolchain, settings); From 522e294e538e085b8d2a2aef821038638f1f613d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Wed, 15 Feb 2023 15:21:22 +0100 Subject: [PATCH 11/42] Restructure ignore files, add comments with reason --- trunk/examples/concurrent/bpl/regression/ignored.txt | 2 +- trunk/examples/concurrent/pthreads/regression/ignored.txt | 1 + .../programs/FloatingPoint/regression/c/ignored.txt | 7 +++++-- .../programs/SignedIntegerOverflow/regression/ignored.txt | 1 + trunk/examples/programs/regression/bpl/ignored.txt | 5 ++++- trunk/examples/programs/regression/c/ignored.txt | 3 +++ 6 files changed, 15 insertions(+), 4 deletions(-) diff --git a/trunk/examples/concurrent/bpl/regression/ignored.txt b/trunk/examples/concurrent/bpl/regression/ignored.txt index 5d7cd7d8cb2..2e58f227dd9 100644 --- a/trunk/examples/concurrent/bpl/regression/ignored.txt +++ b/trunk/examples/concurrent/bpl/regression/ignored.txt @@ -1,6 +1,6 @@ +// Timeout with Automizer, GemCutter succeeds 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 -NonAtomicIncrement_2Threads.c ReachSafety-32bit-Automizer.epf ReachSafety.xml diff --git a/trunk/examples/concurrent/pthreads/regression/ignored.txt b/trunk/examples/concurrent/pthreads/regression/ignored.txt index d6ab96ff834..029dc016dd2 100644 --- a/trunk/examples/concurrent/pthreads/regression/ignored.txt +++ b/trunk/examples/concurrent/pthreads/regression/ignored.txt @@ -1 +1,2 @@ +// Timeout with Automizer, GemCutter succeeds NonAtomicIncrement_2Threads.c ReachSafety-32bit-Automizer.epf ReachSafety.xml diff --git a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt index a4993acc42b..2b302de2dea 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt +++ b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt @@ -1,8 +1,11 @@ +// Timeout BvaddWithThreeArguments.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -SAS09-Float.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml SAS09-Float.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -cbmc_float4_PART1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +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 +cbmc_float4_PART1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml + +// MathSAT does not support quantifiers ctrans-float-rounding.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml cbmc_float-no-simp1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml cbmc_float-to-double2.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml diff --git a/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt b/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt index 6cce0268f0b..d7a5b712499 100644 --- a/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt +++ b/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt @@ -1,2 +1,3 @@ +// Fails due to overapproximation of bitwise operators in the integer translation ShiftLeft06.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml ShiftLeft07.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml diff --git a/trunk/examples/programs/regression/bpl/ignored.txt b/trunk/examples/programs/regression/bpl/ignored.txt index 38341c3da68..26b2b2bf488 100644 --- a/trunk/examples/programs/regression/bpl/ignored.txt +++ b/trunk/examples/programs/regression/bpl/ignored.txt @@ -1,5 +1,8 @@ +// Timeout BugLiveVariables03-Safe.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml -BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml BugNoPredecessorOfReturnTransition.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml nestedWhileSimple-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml + +// The solver is unable to evaluate the formula, PDR cannot handle this +BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml diff --git a/trunk/examples/programs/regression/c/ignored.txt b/trunk/examples/programs/regression/c/ignored.txt index 33479e2ba85..a68ad837ea2 100644 --- a/trunk/examples/programs/regression/c/ignored.txt +++ b/trunk/examples/programs/regression/c/ignored.txt @@ -1,3 +1,4 @@ +// Fails due to overapproximation of bitwise operators in the integer translation BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml BitwiseOperations02.c AutomizerC-forwardPredicates.epf AutomizerC.xml BitwiseOperations02.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml @@ -6,6 +7,8 @@ BitwiseOperations02.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml BitwiseOperations02.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml BitwiseOperations02.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.xml + +// Timeout 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 From ed8ccb92ed3727b19f28c7bd94b2312d71a1a8d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Wed, 15 Feb 2023 16:21:39 +0100 Subject: [PATCH 12/42] Add expected verdict to ignored.txt, only skip with that verdict --- .../concurrent/bpl/regression/ignored.txt | 10 ++-- .../pthreads/regression/ignored.txt | 2 +- .../FloatingPoint/regression/c/ignored.txt | 30 +++++----- .../regression/ignored.txt | 4 +- .../programs/regression/bpl/ignored.txt | 10 ++-- .../programs/regression/c/ignored.txt | 36 ++++++------ .../decider/SafetyCheckTestResultDecider.java | 58 +++++++++---------- .../decider/ThreeTierTestResultDecider.java | 8 +-- .../AbstractRegressionTestSuite.java | 43 +++++++------- ...gieBacktranslationRegressionTestSuite.java | 2 +- .../CBacktranslationRegressionTestSuite.java | 2 +- .../generic/AbsIntRegressionTestSuite.java | 2 +- .../AutomataLibraryRegressionTestSuite.java | 2 +- .../generic/ChcRegressionTestSuite.java | 2 +- .../generic/DataRaceRegressionTestSuite.java | 2 +- .../generic/LTLRegressionTestSuite.java | 2 +- .../generic/MSODRegressionTestSuite.java | 2 +- .../generic/RegressionTestSuite.java | 5 +- .../ReqCheckerRegressionTestSuite.java | 2 +- ...nedIntegerOverflowRegressionTestSuite.java | 5 +- .../TerminationRegressionTestSuite.java | 2 +- .../C2BoogieRegressionTestSuite.java | 2 +- .../LTLTranslationRegressionTestSuite.java | 2 +- 23 files changed, 115 insertions(+), 120 deletions(-) diff --git a/trunk/examples/concurrent/bpl/regression/ignored.txt b/trunk/examples/concurrent/bpl/regression/ignored.txt index 2e58f227dd9..af62a98d004 100644 --- a/trunk/examples/concurrent/bpl/regression/ignored.txt +++ b/trunk/examples/concurrent/bpl/regression/ignored.txt @@ -1,6 +1,6 @@ // Timeout with Automizer, GemCutter succeeds -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 +MirabelleConcurrentIncrement.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT +concurrent_increment.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT +equal-array-sums.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT +loop-lockstep-example.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT +sum_invariant.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT diff --git a/trunk/examples/concurrent/pthreads/regression/ignored.txt b/trunk/examples/concurrent/pthreads/regression/ignored.txt index 029dc016dd2..becc42db31b 100644 --- a/trunk/examples/concurrent/pthreads/regression/ignored.txt +++ b/trunk/examples/concurrent/pthreads/regression/ignored.txt @@ -1,2 +1,2 @@ // Timeout with Automizer, GemCutter succeeds -NonAtomicIncrement_2Threads.c ReachSafety-32bit-Automizer.epf ReachSafety.xml +NonAtomicIncrement_2Threads.c ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT diff --git a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt index 2b302de2dea..c90385358dc 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt +++ b/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt @@ -1,18 +1,18 @@ // Timeout -BvaddWithThreeArguments.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -SAS09-Float.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -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 -cbmc_float4_PART1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +BvaddWithThreeArguments.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml TIMEOUT +SAS09-Float.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml TIMEOUT +SAS09-Float.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml TIMEOUT +ctrans-float-rounding.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml TIMEOUT +cbmc_float4_PART1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml TIMEOUT // MathSAT does not support quantifiers -ctrans-float-rounding.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -cbmc_float-no-simp1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -cbmc_float-to-double2.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -cbmc_float12.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -cbmc_float13.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -cbmc_float19.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -cbmc_float20_Part1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -cbmc_float20_Part3.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -cbmc_float6.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml -QuantifiedFloatInvariant.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml +ctrans-float-rounding.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR +cbmc_float-no-simp1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR +cbmc_float-to-double2.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR +cbmc_float12.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR +cbmc_float13.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR +cbmc_float19.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR +cbmc_float20_Part1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR +cbmc_float20_Part3.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR +cbmc_float6.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR +QuantifiedFloatInvariant.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR diff --git a/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt b/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt index d7a5b712499..6da0e411e33 100644 --- a/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt +++ b/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt @@ -1,3 +1,3 @@ // Fails due to overapproximation of bitwise operators in the integer translation -ShiftLeft06.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml -ShiftLeft07.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml +ShiftLeft06.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml UNKNOWN +ShiftLeft07.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml UNKNOWN diff --git a/trunk/examples/programs/regression/bpl/ignored.txt b/trunk/examples/programs/regression/bpl/ignored.txt index 26b2b2bf488..e98a3b9ef2b 100644 --- a/trunk/examples/programs/regression/bpl/ignored.txt +++ b/trunk/examples/programs/regression/bpl/ignored.txt @@ -1,8 +1,8 @@ // 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 +BugLiveVariables03-Safe.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml TIMEOUT +BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml TIMEOUT +BugNoPredecessorOfReturnTransition.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT +nestedWhileSimple-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT // The solver is unable to evaluate the formula, PDR cannot handle this -BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml +BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml EXCEPTION_OR_ERROR diff --git a/trunk/examples/programs/regression/c/ignored.txt b/trunk/examples/programs/regression/c/ignored.txt index a68ad837ea2..d937633d23b 100644 --- a/trunk/examples/programs/regression/c/ignored.txt +++ b/trunk/examples/programs/regression/c/ignored.txt @@ -1,21 +1,21 @@ // Fails due to overapproximation of bitwise operators in the integer translation -BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.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-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml -BitwiseOperations02.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml -BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.xml +BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN +BitwiseOperations02.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN // Timeout -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 -array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml -array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml +ShortCircuit-SideEffect-DoStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +ShortCircuit-SideEffect-ForStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c AutomizerC-forwardPredicates.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml TIMEOUT +array10_pattern_simplified.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml TIMEOUT +array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml TIMEOUT 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 5d2b2b39a63..045bb2c4821 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 @@ -31,6 +31,7 @@ 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; +import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.IExpectedResultFinder.ExpectedResultFinderStatus; import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.KeywordBasedExpectedResultFinder; import de.uni_freiburg.informatik.ultimate.test.decider.overallresult.IOverallResultEvaluator; import de.uni_freiburg.informatik.ultimate.test.decider.overallresult.SafetyCheckerOverallResult; @@ -54,8 +55,8 @@ public class SafetyCheckTestResultDecider extends ThreeTierTestResultDecider expectedResultFinder, final IOverallResultEvaluator overallResultDeterminer) { - evaluateExpectedResult(expectedResultFinder); - switch (expectedResultFinder.getExpectedResultFinderStatus()) { - case ERROR: - // we will not evaluate overall result; - return; - case EXPECTED_RESULT_FOUND: - compareToOverallResult(expectedResultFinder.getExpectedResult(), overallResultDeterminer); - return; - case NO_EXPECTED_RESULT_FOUND: - evaluateOverallResultWithoutExpectedResult(overallResultDeterminer); - return; - default: - throw new IllegalArgumentException(); + + final ExpectedResultFinderStatus status = expectedResultFinder.getExpectedResultFinderStatus(); + if (mOverridenExpectedVerdict != null) { + final SafetyCheckerOverallResult expectedVerdict = + SafetyCheckerOverallResult.valueOf(mOverridenExpectedVerdict); + mMessage = "ExpectedResult (overriden): " + expectedVerdict; + compareToOverallResult(expectedVerdict, overallResultDeterminer, true); + } else { + evaluateExpectedResult(expectedResultFinder); + if (status == ExpectedResultFinderStatus.NO_EXPECTED_RESULT_FOUND) { + evaluateOverallResultWithoutExpectedResult(overallResultDeterminer); + } else if (status == ExpectedResultFinderStatus.EXPECTED_RESULT_FOUND) { + compareToOverallResult(expectedResultFinder.getExpectedResult(), overallResultDeterminer, false); + } } } @@ -117,10 +119,6 @@ private void evaluateOverallResultWithoutExpectedResult( mCategory = overallResult + " (Expected:UNKNOWN)"; mMessage += " UltimateResult: " + overallResultMsg; - if (mIsIgnored) { - mTestResult = TestResult.IGNORE; - return; - } switch (overallResult) { case EXCEPTION_OR_ERROR: case UNSUPPORTED_SYNTAX: @@ -144,7 +142,8 @@ private void evaluateOverallResultWithoutExpectedResult( } private void compareToOverallResult(final SafetyCheckerOverallResult expectedResult, - final IOverallResultEvaluator overallResultDeterminer) { + final IOverallResultEvaluator overallResultDeterminer, + final boolean skipOnSuccess) { final SafetyCheckerOverallResult overallResult = overallResultDeterminer.getOverallResult(); final String overallResultMsg = overallResultDeterminer.generateOverallResultMessage(); @@ -153,7 +152,7 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes switch (overallResult) { case EXCEPTION_OR_ERROR: mCategory = overallResult + " (Expected:" + expectedResult + ") " + overallResultMsg; - mTestResult = mIsIgnored ? TestResult.IGNORE : TestResult.FAIL; + mTestResult = skipOnSuccess && expectedResult == overallResult ? TestResult.IGNORE : TestResult.FAIL; break; case SAFE: if (expectedResult == SafetyCheckerOverallResult.SAFE) { @@ -176,11 +175,11 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes break; case UNSAFE_OVERAPPROXIMATED: if (expectedResult == overallResult) { - mTestResult = TestResult.SUCCESS; + mTestResult = skipOnSuccess ? TestResult.IGNORE : TestResult.SUCCESS; } else if (expectedResult == SafetyCheckerOverallResult.UNSAFE) { mTestResult = TestResult.SUCCESS; } else { - mTestResult = mIsIgnored ? TestResult.IGNORE : TestResult.UNKNOWN; + mTestResult = TestResult.UNKNOWN; } break; case INVALID_ANNOTATION: @@ -192,11 +191,14 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes } break; case UNKNOWN: + case TIMEOUT: // syntax error should always have been found if (expectedResult == SafetyCheckerOverallResult.SYNTAX_ERROR) { mTestResult = TestResult.FAIL; + } else if (skipOnSuccess && expectedResult == overallResult) { + mTestResult = TestResult.IGNORE; } else { - mTestResult = mIsIgnored ? TestResult.IGNORE : TestResult.UNKNOWN; + mTestResult = TestResult.UNKNOWN; } break; case SYNTAX_ERROR: @@ -206,14 +208,6 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes mTestResult = TestResult.FAIL; } break; - case TIMEOUT: - // syntax error should always have been found - if (expectedResult == SafetyCheckerOverallResult.SYNTAX_ERROR) { - mTestResult = TestResult.FAIL; - } else { - mTestResult = mIsIgnored ? TestResult.IGNORE : TestResult.UNKNOWN; - } - break; case UNSUPPORTED_SYNTAX: mTestResult = TestResult.FAIL; break; 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 443e06ef4e7..13498aeb033 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,7 +59,7 @@ public abstract class ThreeTierTestResultDecider implements ITes private final IExpectedResultFinder mExpectedResultEvaluation; private IOverallResultEvaluator mUltimateResultEvaluation; private ITestResultEvaluation mTestResultEvaluation; - protected boolean mIsIgnored; + protected final String mOverridenExpectedVerdict; /** * @@ -73,9 +73,9 @@ public abstract class ThreeTierTestResultDecider implements ITes * Is the test case ignored? */ public ThreeTierTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, - final boolean unknownIsJUnitSuccess, final boolean isIgnored) { + final boolean unknownIsJUnitSuccess, final String overridenExpectedVerdict) { mUnknownIsJUnitSuccess = unknownIsJUnitSuccess; - mIsIgnored = isIgnored; + mOverridenExpectedVerdict = overridenExpectedVerdict; mUltimateRunDefinition = ultimateRunDefinition; mExpectedResultEvaluation = constructExpectedResultFinder(); mExpectedResultEvaluation.findExpectedResult(ultimateRunDefinition); @@ -91,7 +91,7 @@ public ThreeTierTestResultDecider(final UltimateRunDefinition ultimateRunDefinit */ public ThreeTierTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, final boolean unknownIsJUnitSuccess) { - this(ultimateRunDefinition, unknownIsJUnitSuccess, false); + this(ultimateRunDefinition, unknownIsJUnitSuccess, null); } @Override 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 4a51d39f16a..0c296be334a 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 @@ -52,7 +52,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.Triple; +import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.NestedMap3; /** * An {@link AbstractRegressionTestSuite} is a {@link UltimateTestSuite} that automatically generates tests from folders @@ -116,66 +116,64 @@ public Collection createTestCases() { for (final Config runConfiguration : runConfigurations) { final Collection inputFiles = getInputFiles(filesRegexFilter, runConfiguration); // TODO: Better path - final Set> ignoredTestFails = + final NestedMap3 ignoredTestFails = getIgnoredTestFails(new File(runConfiguration.getSettingsFile().getParentFile(), "ignored.txt")); for (final File inputFile : inputFiles) { final UltimateRunDefinition urd = new UltimateRunDefinition(inputFile, runConfiguration.getSettingsFile(), runConfiguration.getToolchainFile(), getTimeout(runConfiguration, inputFile)); - final boolean isIgnored = ignoredTestFails.contains(new Triple<>(inputFile.getName(), - runConfiguration.getSettingsFile().getName(), runConfiguration.getToolchainFile().getName())); - rtr.add(buildTestCase(urd, getTestResultDecider(urd, isIgnored))); + final String overridenVerdict = ignoredTestFails.get(inputFile.getName(), + runConfiguration.getSettingsFile().getName(), runConfiguration.getToolchainFile().getName()); + rtr.add(buildTestCase(urd, getTestResultDecider(urd, overridenVerdict))); } } return rtr; } - private static Set> getIgnoredTestFails(final File ignoreFile) { - final Set> ignoredTestFails = new HashSet<>(); + private static NestedMap3 getIgnoredTestFails(final File ignoreFile) { + final NestedMap3 result = new NestedMap3<>(); try (BufferedReader br = new BufferedReader(new InputStreamReader(new FileInputStream(ignoreFile)))) { String line; while ((line = br.readLine()) != null) { - final Triple triple = parseIgnoreLine(line); - if (triple != null) { - ignoredTestFails.add(triple); - } + addIgnoreLine(line, result); } } catch (final IOException e) { // Just skip } - return ignoredTestFails; + return result; } - private static Triple parseIgnoreLine(final String line) { + private static void addIgnoreLine(final String line, final NestedMap3 map) { if (line.startsWith("//")) { - return null; + return; } String settings = null; String toolchain = null; String file = null; final String[] args = line.split("\\s+"); - if (args.length != 3) { - return null; + if (args.length != 4) { + return; } - for (final String arg : args) { + for (int i = 0; i < 3; i++) { + final String arg = args[i]; if (arg.endsWith(".epf")) { if (settings != null) { - return null; + return; } settings = arg; } else if (arg.endsWith(".xml")) { if (toolchain != null) { - return null; + return; } toolchain = arg; } else { if (file != null) { - return null; + return; } file = arg; } } - return new Triple<>(file, settings, toolchain); + map.put(file, settings, toolchain, args[3]); } protected long getTimeout(final Config rundef, final File file) { @@ -321,7 +319,8 @@ protected Collection getInputFiles(final Predicate regexFilter, fina .collect(Collectors.toList()); } - protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition, boolean isIgnored); + protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition, + String overridenExpectedVerdict); 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/backtranslation/BoogieBacktranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java index 6b958902198..54afb6f7e4a 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java @@ -46,7 +46,7 @@ public BoogieBacktranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new BacktranslationTestResultDecider(runDefinition); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java index ccba31b164a..47674066717 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java @@ -46,7 +46,7 @@ public CBacktranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new BacktranslationTestResultDecider(runDefinition); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java index 24abd35bbd1..bfe40918a2e 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java @@ -51,7 +51,7 @@ public AbsIntRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new OverapproximatingSafetyCheckTestResultDecider(runDefinition, true); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java index c17116f91b6..e028e2f4476 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java @@ -50,7 +50,7 @@ public AutomataLibraryRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new AutomataScriptTestResultDecider(); } 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 c9fd2b9e739..10f00af9c40 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 @@ -57,7 +57,7 @@ public ChcRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { 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 b35bc7f8a48..b9e6bdad9e1 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 @@ -56,7 +56,7 @@ public DataRaceRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new SafetyCheckTestResultDecider(runDefinition, false); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java index 3c316d72e5c..ec00b8b95ea 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java @@ -49,7 +49,7 @@ public LTLRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new LTLCheckerTestResultDecider(runDefinition, false); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java index 67f47fc8341..c4f76a4f26b 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java @@ -51,7 +51,7 @@ public MSODRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { final boolean unknownIsSuccess = true; return new MSODTestResultDecider(runDefinition, unknownIsSuccess); } 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 3a72b11c26a..ef50d57a715 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 @@ -54,8 +54,9 @@ public RegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final boolean isIgnored) { - return new SafetyCheckTestResultDecider(runDefinition, false, isIgnored); + 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/ReqCheckerRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java index 73fb831f66b..2bb43f0f72d 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java @@ -79,7 +79,7 @@ public ReqCheckerRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new ReqCheckerTestResultDecider(runDefinition, false); } 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 d49cb4fd1be..996a4548d76 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 @@ -48,8 +48,9 @@ public SignedIntegerOverflowRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final boolean isIgnored) { - return new SafetyCheckTestResultDecider(runDefinition, false, isIgnored); + 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 c4b3a9260ed..84e330e7938 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 @@ -50,7 +50,7 @@ public TerminationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new TerminationAnalysisTestResultDecider(runDefinition, false); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java index 53c0b245d09..c3cf516d455 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java @@ -66,7 +66,7 @@ public C2BoogieRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new TranslationTestResultDecider(runDefinition.selectPrimaryInputFile()); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java index 28d0d5314fd..63f282d019b 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java @@ -48,7 +48,7 @@ public LTLTranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, boolean isIgnored) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { return new TranslationTestResultDecider(runDefinition.selectPrimaryInputFile()); } From dbd795ab6b36f2d773f63be14c94e1f4bb9c3675 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Thu, 16 Feb 2023 14:14:47 +0100 Subject: [PATCH 13/42] Fix some expected verdicts --- trunk/examples/programs/regression/c/ignored.txt | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/trunk/examples/programs/regression/c/ignored.txt b/trunk/examples/programs/regression/c/ignored.txt index d937633d23b..cad11035d36 100644 --- a/trunk/examples/programs/regression/c/ignored.txt +++ b/trunk/examples/programs/regression/c/ignored.txt @@ -1,14 +1,14 @@ // Fails due to overapproximation of bitwise operators in the integer translation -BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN BitwiseOperations02.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN BitwiseOperations02.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN BitwiseOperations02.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN BitwiseOperations02.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN -BitwiseOperations02.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN BitwiseOperations02.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN // Timeout +BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +BitwiseOperations02.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT ShortCircuit-SideEffect-DoStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT ShortCircuit-SideEffect-ForStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT StructPositiveSum-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT @@ -17,5 +17,7 @@ StructPositiveSum-Safe.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml T StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml TIMEOUT array10_pattern_simplified.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml TIMEOUT -array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml TIMEOUT + +// Unable to decide satisfiability of path constraint +array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN From bcbff5637592e269662027de9fd514e0e4a4658d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Thu, 16 Feb 2023 14:21:22 +0100 Subject: [PATCH 14/42] Catch case where String cannot be converted to enum --- .../decider/SafetyCheckTestResultDecider.java | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) 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 045bb2c4821..66bd4813779 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 @@ -87,6 +87,18 @@ public ITestResultEvaluation constructTestResultEval return new SafetyCheckerTestResultEvaluation(); } + private SafetyCheckerOverallResult getOverridenExpectedVerdict() { + if (mOverridenExpectedVerdict == null) { + return null; + } + try { + return SafetyCheckerOverallResult.valueOf(mOverridenExpectedVerdict); + } catch (final IllegalArgumentException e) { + // Cannot convert to SafetyCheckerOverallResult, fall back to provided expected result + return null; + } + } + public class SafetyCheckerTestResultEvaluation implements ITestResultEvaluation { private String mCategory; private String mMessage; @@ -97,9 +109,8 @@ public void evaluateTestResult(final IExpectedResultFinder overallResultDeterminer) { final ExpectedResultFinderStatus status = expectedResultFinder.getExpectedResultFinderStatus(); - if (mOverridenExpectedVerdict != null) { - final SafetyCheckerOverallResult expectedVerdict = - SafetyCheckerOverallResult.valueOf(mOverridenExpectedVerdict); + final SafetyCheckerOverallResult expectedVerdict = getOverridenExpectedVerdict(); + if (expectedVerdict != null) { mMessage = "ExpectedResult (overriden): " + expectedVerdict; compareToOverallResult(expectedVerdict, overallResultDeterminer, true); } else { From adde04c0228e134a8e1c18e3595b4c4f3583361f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Thu, 16 Feb 2023 14:22:58 +0100 Subject: [PATCH 15/42] Minor: Restructure method --- .../decider/SafetyCheckTestResultDecider.java | 25 +++++++++++-------- 1 file changed, 15 insertions(+), 10 deletions(-) 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 66bd4813779..140f4d7c203 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 @@ -31,7 +31,6 @@ 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; -import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.IExpectedResultFinder.ExpectedResultFinderStatus; import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.KeywordBasedExpectedResultFinder; import de.uni_freiburg.informatik.ultimate.test.decider.overallresult.IOverallResultEvaluator; import de.uni_freiburg.informatik.ultimate.test.decider.overallresult.SafetyCheckerOverallResult; @@ -107,19 +106,25 @@ public class SafetyCheckerTestResultEvaluation implements ITestResultEvaluation< @Override public void evaluateTestResult(final IExpectedResultFinder expectedResultFinder, final IOverallResultEvaluator overallResultDeterminer) { - - final ExpectedResultFinderStatus status = expectedResultFinder.getExpectedResultFinderStatus(); final SafetyCheckerOverallResult expectedVerdict = getOverridenExpectedVerdict(); if (expectedVerdict != null) { mMessage = "ExpectedResult (overriden): " + expectedVerdict; compareToOverallResult(expectedVerdict, overallResultDeterminer, true); - } else { - evaluateExpectedResult(expectedResultFinder); - if (status == ExpectedResultFinderStatus.NO_EXPECTED_RESULT_FOUND) { - evaluateOverallResultWithoutExpectedResult(overallResultDeterminer); - } else if (status == ExpectedResultFinderStatus.EXPECTED_RESULT_FOUND) { - compareToOverallResult(expectedResultFinder.getExpectedResult(), overallResultDeterminer, false); - } + return; + } + evaluateExpectedResult(expectedResultFinder); + switch (expectedResultFinder.getExpectedResultFinderStatus()) { + case ERROR: + // we will not evaluate overall result; + return; + case EXPECTED_RESULT_FOUND: + compareToOverallResult(expectedResultFinder.getExpectedResult(), overallResultDeterminer, false); + return; + case NO_EXPECTED_RESULT_FOUND: + evaluateOverallResultWithoutExpectedResult(overallResultDeterminer); + return; + default: + throw new IllegalArgumentException(); } } From 6362e6a46992623f9d161bf113273572e742b05c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Thu, 16 Feb 2023 14:26:02 +0100 Subject: [PATCH 16/42] Fix documentation --- .../ultimate/test/decider/SafetyCheckTestResultDecider.java | 3 +++ .../ultimate/test/decider/ThreeTierTestResultDecider.java | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) 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 140f4d7c203..ce8711eec87 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 @@ -52,6 +52,9 @@ public class SafetyCheckTestResultDecider extends ThreeTierTestResultDecider implements ITes * if true the TestResult UNKNOWN is a success for JUnit, if false, the TestResult UNKNOWN is a failure * for JUnit. * - * @param isIgnored - * Is the test case ignored? + * @param overridenExpectedVerdict + * The expected verdict overridden in a separate file, null if not present. */ public ThreeTierTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, final boolean unknownIsJUnitSuccess, final String overridenExpectedVerdict) { From 66815b3b75b4d88543c9b6389bbdbd3c6aab31c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 28 Feb 2023 14:36:02 +0100 Subject: [PATCH 17/42] Rename ignored.txt to .skip --- trunk/examples/concurrent/bpl/regression/{ignored.txt => .skip} | 0 .../concurrent/pthreads/regression/{ignored.txt => .skip} | 0 .../programs/FloatingPoint/regression/c/{ignored.txt => .skip} | 0 .../SignedIntegerOverflow/regression/{ignored.txt => .skip} | 0 trunk/examples/programs/regression/bpl/{ignored.txt => .skip} | 0 trunk/examples/programs/regression/c/{ignored.txt => .skip} | 0 .../ultimate/regressiontest/AbstractRegressionTestSuite.java | 2 +- 7 files changed, 1 insertion(+), 1 deletion(-) rename trunk/examples/concurrent/bpl/regression/{ignored.txt => .skip} (100%) rename trunk/examples/concurrent/pthreads/regression/{ignored.txt => .skip} (100%) rename trunk/examples/programs/FloatingPoint/regression/c/{ignored.txt => .skip} (100%) rename trunk/examples/programs/SignedIntegerOverflow/regression/{ignored.txt => .skip} (100%) rename trunk/examples/programs/regression/bpl/{ignored.txt => .skip} (100%) rename trunk/examples/programs/regression/c/{ignored.txt => .skip} (100%) diff --git a/trunk/examples/concurrent/bpl/regression/ignored.txt b/trunk/examples/concurrent/bpl/regression/.skip similarity index 100% rename from trunk/examples/concurrent/bpl/regression/ignored.txt rename to trunk/examples/concurrent/bpl/regression/.skip diff --git a/trunk/examples/concurrent/pthreads/regression/ignored.txt b/trunk/examples/concurrent/pthreads/regression/.skip similarity index 100% rename from trunk/examples/concurrent/pthreads/regression/ignored.txt rename to trunk/examples/concurrent/pthreads/regression/.skip diff --git a/trunk/examples/programs/FloatingPoint/regression/c/ignored.txt b/trunk/examples/programs/FloatingPoint/regression/c/.skip similarity index 100% rename from trunk/examples/programs/FloatingPoint/regression/c/ignored.txt rename to trunk/examples/programs/FloatingPoint/regression/c/.skip diff --git a/trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt b/trunk/examples/programs/SignedIntegerOverflow/regression/.skip similarity index 100% rename from trunk/examples/programs/SignedIntegerOverflow/regression/ignored.txt rename to trunk/examples/programs/SignedIntegerOverflow/regression/.skip diff --git a/trunk/examples/programs/regression/bpl/ignored.txt b/trunk/examples/programs/regression/bpl/.skip similarity index 100% rename from trunk/examples/programs/regression/bpl/ignored.txt rename to trunk/examples/programs/regression/bpl/.skip diff --git a/trunk/examples/programs/regression/c/ignored.txt b/trunk/examples/programs/regression/c/.skip similarity index 100% rename from trunk/examples/programs/regression/c/ignored.txt rename to trunk/examples/programs/regression/c/.skip 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 0c296be334a..2b9ba8ab6fc 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 @@ -117,7 +117,7 @@ public Collection createTestCases() { final Collection inputFiles = getInputFiles(filesRegexFilter, runConfiguration); // TODO: Better path final NestedMap3 ignoredTestFails = - getIgnoredTestFails(new File(runConfiguration.getSettingsFile().getParentFile(), "ignored.txt")); + getIgnoredTestFails(new File(runConfiguration.getSettingsFile().getParentFile(), ".skip")); for (final File inputFile : inputFiles) { final UltimateRunDefinition urd = new UltimateRunDefinition(inputFile, runConfiguration.getSettingsFile(), From 4de4c3f49b423b438d568e6724025eef662ded07 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 28 Feb 2023 14:45:40 +0100 Subject: [PATCH 18/42] Refactoring, allow .skip file in toolchain and settings dir --- .../AbstractRegressionTestSuite.java | 29 ++++++++++++++----- 1 file changed, 21 insertions(+), 8 deletions(-) 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 2b9ba8ab6fc..a3f8d4b8a1a 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 @@ -67,6 +67,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 = ".skip"; protected long mTimeout; protected String mRootFolder; @@ -115,14 +116,12 @@ public Collection createTestCases() { final Predicate filesRegexFilter = getFilesRegexFilter(); for (final Config runConfiguration : runConfigurations) { final Collection inputFiles = getInputFiles(filesRegexFilter, runConfiguration); - // TODO: Better path - final NestedMap3 ignoredTestFails = - getIgnoredTestFails(new File(runConfiguration.getSettingsFile().getParentFile(), ".skip")); + final NestedMap3 skippedTests = getSkippedTests(runConfiguration); for (final File inputFile : inputFiles) { final UltimateRunDefinition urd = new UltimateRunDefinition(inputFile, runConfiguration.getSettingsFile(), runConfiguration.getToolchainFile(), getTimeout(runConfiguration, inputFile)); - final String overridenVerdict = ignoredTestFails.get(inputFile.getName(), + final String overridenVerdict = skippedTests.get(inputFile.getName(), runConfiguration.getSettingsFile().getName(), runConfiguration.getToolchainFile().getName()); rtr.add(buildTestCase(urd, getTestResultDecider(urd, overridenVerdict))); } @@ -130,20 +129,34 @@ public Collection createTestCases() { return rtr; } - private static NestedMap3 getIgnoredTestFails(final File ignoreFile) { + private static NestedMap3 getSkippedTests(final Config runConfiguration) { final NestedMap3 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); + } + return result; + } + + private static void addSkippedTest(final File ignoreFile, final NestedMap3 map) { try (BufferedReader br = new BufferedReader(new InputStreamReader(new FileInputStream(ignoreFile)))) { String line; while ((line = br.readLine()) != null) { - addIgnoreLine(line, result); + addSkipLine(line, map); } } catch (final IOException e) { // Just skip } - return result; } - private static void addIgnoreLine(final String line, final NestedMap3 map) { + private static void addSkipLine(final String line, final NestedMap3 map) { if (line.startsWith("//")) { return; } From 75786af9bd1c6fb3b6843bc9bafee4eba7f6437b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Fri, 5 May 2023 14:00:05 +0200 Subject: [PATCH 19/42] Skip tests with overapproximation --- trunk/examples/programs/quantifier/regression/bpl/.skip | 2 ++ trunk/examples/programs/regression/bpl/.skip | 6 ++++++ 2 files changed, 8 insertions(+) create mode 100644 trunk/examples/programs/quantifier/regression/bpl/.skip diff --git a/trunk/examples/programs/quantifier/regression/bpl/.skip b/trunk/examples/programs/quantifier/regression/bpl/.skip new file mode 100644 index 00000000000..b524850b8a7 --- /dev/null +++ b/trunk/examples/programs/quantifier/regression/bpl/.skip @@ -0,0 +1,2 @@ +// Overapproximation +AuxVarInCall.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml UNKNOWN diff --git a/trunk/examples/programs/regression/bpl/.skip b/trunk/examples/programs/regression/bpl/.skip index e98a3b9ef2b..592e468dc0b 100644 --- a/trunk/examples/programs/regression/bpl/.skip +++ b/trunk/examples/programs/regression/bpl/.skip @@ -4,5 +4,11 @@ BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf Automizer BugNoPredecessorOfReturnTransition.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT nestedWhileSimple-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT +// Overapproximation +Overapproximation.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml UNKNOWN +Overapproximation.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml UNKNOWN +Overapproximation.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml UNKNOWN +Overapproximation.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml UNKNOWN + // The solver is unable to evaluate the formula, PDR cannot handle this BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml EXCEPTION_OR_ERROR From fcfd79afb306026509655d1814bfb923575d225b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Mon, 19 Aug 2024 17:27:15 +0200 Subject: [PATCH 20/42] Fix build in new regression tests --- .../generic/ReqCheckerRedundancyRegressionTestSuite.java | 6 ++++-- .../regressiontest/generic/WitnessRegressionTestSuite.java | 5 +++-- 2 files changed, 7 insertions(+), 4 deletions(-) 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..72bfa775883 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 @@ -76,7 +76,8 @@ public ReqCheckerRedundancyRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { return new ReqCheckerTestResultDecider(runDefinition, false); } @@ -173,7 +174,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/WitnessRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java index 1d5d85f033c..6a8ff8f0345 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java @@ -61,7 +61,8 @@ public WitnessRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { return new WitnessSafetyCheckTestResultDecider(runDefinition); } @@ -77,7 +78,7 @@ public Collection createTestCases() { final File[] newFiles = DataStructureUtils.concat(def.getInput(), new File[] { witness }); final UltimateRunDefinition newDef = new UltimateRunDefinition(newFiles, def.getSettings(), def.getToolchain(), def.getTimeout()); - result.add(new UltimateTestCase(getTestResultDecider(def), newDef, List.of(), null)); + result.add(new UltimateTestCase(getTestResultDecider(def, null), newDef, List.of(), null)); } } } From fa6fc5faaac652cdaf22b28ae1a9729729bac2d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 10:00:56 +0200 Subject: [PATCH 21/42] Throw exception when testsuite does not support skipping tests --- .../regressiontest/AbstractRegressionTestSuite.java | 6 ++++++ .../BoogieBacktranslationRegressionTestSuite.java | 4 +++- .../CBacktranslationRegressionTestSuite.java | 4 +++- .../regressiontest/generic/AbsIntRegressionTestSuite.java | 4 +++- .../generic/AutomataLibraryRegressionTestSuite.java | 4 +++- .../regressiontest/generic/ChcRegressionTestSuite.java | 6 ++++-- .../regressiontest/generic/DataRaceRegressionTestSuite.java | 4 +++- .../regressiontest/generic/LTLRegressionTestSuite.java | 4 +++- .../regressiontest/generic/MSODRegressionTestSuite.java | 4 +++- .../generic/ReqCheckerRedundancyRegressionTestSuite.java | 1 + .../generic/ReqCheckerRegressionTestSuite.java | 4 +++- .../generic/TerminationRegressionTestSuite.java | 4 +++- .../regressiontest/generic/WitnessRegressionTestSuite.java | 1 + 13 files changed, 39 insertions(+), 11 deletions(-) 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 a3f8d4b8a1a..09fd5895210 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 @@ -335,6 +335,12 @@ protected Collection getInputFiles(final Predicate 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 { diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java index 54afb6f7e4a..7457bdb0491 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/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/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java index 47674066717..6a53cab2a53 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/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/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java index bfe40918a2e..58e298a6180 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/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/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java index e028e2f4476..71043cb1e99 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/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/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 10f00af9c40..a3ef71342b0 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 @@ -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/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 b9e6bdad9e1..1067045cde3 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 @@ -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/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java index ec00b8b95ea..63697973ced 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/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/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java index c4f76a4f26b..cde8e97e7bc 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/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/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 72bfa775883..4849dad0506 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 @@ -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/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java index 2bb43f0f72d..4032ec22066 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_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/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 84e330e7938..541263435ee 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 @@ -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/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java index 6a8ff8f0345..c0a8a3d6cf4 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/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); } From b03532f1d2ddb2595dd550893097f5a44d165435 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 10:47:48 +0200 Subject: [PATCH 22/42] Update .skip files --- .../programs/FloatingPoint/regression/c/.skip | 15 ----- trunk/examples/programs/regression/bpl/.skip | 56 ++++++++++++++++++- 2 files changed, 55 insertions(+), 16 deletions(-) diff --git a/trunk/examples/programs/FloatingPoint/regression/c/.skip b/trunk/examples/programs/FloatingPoint/regression/c/.skip index c90385358dc..ecc7d7e059b 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/.skip +++ b/trunk/examples/programs/FloatingPoint/regression/c/.skip @@ -1,18 +1,3 @@ // Timeout -BvaddWithThreeArguments.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml TIMEOUT -SAS09-Float.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml TIMEOUT SAS09-Float.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml TIMEOUT ctrans-float-rounding.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml TIMEOUT -cbmc_float4_PART1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml TIMEOUT - -// MathSAT does not support quantifiers -ctrans-float-rounding.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float-no-simp1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float-to-double2.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float12.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float13.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float19.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float20_Part1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float20_Part3.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float6.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -QuantifiedFloatInvariant.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR diff --git a/trunk/examples/programs/regression/bpl/.skip b/trunk/examples/programs/regression/bpl/.skip index 592e468dc0b..198a9ebe130 100644 --- a/trunk/examples/programs/regression/bpl/.skip +++ b/trunk/examples/programs/regression/bpl/.skip @@ -3,8 +3,54 @@ BugLiveVariables03-Safe.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml TIMEOUT BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml TIMEOUT BugNoPredecessorOfReturnTransition.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT nestedWhileSimple-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT +array10_pattern_simplified.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +BitwiseOperations02.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +Acsl01-EnsuresLocal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +Acsl03-EnsuresGlobal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +Tschingelhorn-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +ShortCircuit-SideEffect-DoStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +ShortCircuit-SideEffect-ForStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c AutomizerC-forwardPredicates.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -// Overapproximation +// Unknown, overapproximation of bitwise operations (for integer translation) +bitwiseOrUnsigned.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN +builtin_ffs.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +builtin_ffs.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +builtin_ffs.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +builtin_ffs.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +builtin_ffs.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN +builtin_ffs.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN + +// Unknown, unable to decide satisfiability of path constraint +array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN + +// Overapproximation, we expect unknown for Automizer Overapproximation.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml UNKNOWN Overapproximation.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml UNKNOWN Overapproximation.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml UNKNOWN @@ -12,3 +58,11 @@ Overapproximation.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml UNKNOWN // The solver is unable to evaluate the formula, PDR cannot handle this BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml EXCEPTION_OR_ERROR + +// We are unable to backtranslate @diff from SMT to Boogie +BugLiveVariables03-Safe.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml EXCEPTION_OR_ERROR +BugLiveVariables04-Safe.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml EXCEPTION_OR_ERROR + +// Const is only supported for infinite index sort in SMTInterpol +ConstArray.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml EXCEPTION_OR_ERROR +ConstArray.bpl AutomizerBpl-nestedInterpolants.epf PdrAutomizerBpl.xml EXCEPTION_OR_ERROR From 9189631378afe24961429b647c4cf85d7363718f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 10:52:52 +0200 Subject: [PATCH 23/42] Skip data race tests --- .../pthreads/races/regression/.skip | 7 ++++++ .../generic/DataRaceRegressionTestSuite.java | 23 +------------------ 2 files changed, 8 insertions(+), 22 deletions(-) create mode 100644 trunk/examples/concurrent/pthreads/races/regression/.skip diff --git a/trunk/examples/concurrent/pthreads/races/regression/.skip b/trunk/examples/concurrent/pthreads/races/regression/.skip new file mode 100644 index 00000000000..6f17d13b14a --- /dev/null +++ b/trunk/examples/concurrent/pthreads/races/regression/.skip @@ -0,0 +1,7 @@ +// Timeout +static-array-copy3.c DataRace-32bit-Automizer_Bitvector.epf DataRace.xml TIMEOUT +static-array-copy3.c DataRace-32bit-Automizer_Default.epf DataRace.xml TIMEOUT +static-array-copy3.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml TIMEOUT + +// Crash in MathSAT +static-array-write.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml EXCEPTION_OR_ERROR 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 1067045cde3..b2312669680 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,32 +38,16 @@ 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 protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); - return new SafetyCheckTestResultDecider(runDefinition, false); - } - - @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); + return new SafetyCheckTestResultDecider(runDefinition, false, overridenExpectedVerdict); } } From 2467d4a49b83c62d3f82cbea9c088a0b4940d274 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 11:07:54 +0200 Subject: [PATCH 24/42] Fix updating wrong .skip file --- trunk/examples/programs/regression/bpl/.skip | 46 -------------------- trunk/examples/programs/regression/c/.skip | 25 +++++++++++ 2 files changed, 25 insertions(+), 46 deletions(-) diff --git a/trunk/examples/programs/regression/bpl/.skip b/trunk/examples/programs/regression/bpl/.skip index 198a9ebe130..844306912f7 100644 --- a/trunk/examples/programs/regression/bpl/.skip +++ b/trunk/examples/programs/regression/bpl/.skip @@ -3,52 +3,6 @@ BugLiveVariables03-Safe.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml TIMEOUT BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml TIMEOUT BugNoPredecessorOfReturnTransition.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT nestedWhileSimple-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT -array10_pattern_simplified.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -BitwiseOperations02.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -Acsl01-EnsuresLocal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -Acsl03-EnsuresGlobal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -Tschingelhorn-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -ShortCircuit-SideEffect-DoStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -ShortCircuit-SideEffect-ForStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c AutomizerC-forwardPredicates.epf AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT - -// Unknown, overapproximation of bitwise operations (for integer translation) -bitwiseOrUnsigned.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN -builtin_ffs.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN -builtin_ffs.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN -builtin_ffs.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -builtin_ffs.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN -builtin_ffs.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN -builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN -builtin_ffs.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN -BitwiseOperations02.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN -BitwiseOperations02.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN -BitwiseOperations02.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -BitwiseOperations02.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN -BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN - -// Unknown, unable to decide satisfiability of path constraint -array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN // Overapproximation, we expect unknown for Automizer Overapproximation.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml UNKNOWN diff --git a/trunk/examples/programs/regression/c/.skip b/trunk/examples/programs/regression/c/.skip index cad11035d36..92cdd01f3ad 100644 --- a/trunk/examples/programs/regression/c/.skip +++ b/trunk/examples/programs/regression/c/.skip @@ -1,4 +1,24 @@ // Fails due to overapproximation of bitwise operators in the integer translation +bitwiseOrUnsigned.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN +builtin_ffs.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +builtin_ffs.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +builtin_ffs.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +builtin_ffs.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +builtin_ffs.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN +builtin_ffs.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN BitwiseOperations02.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN BitwiseOperations02.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN BitwiseOperations02.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN @@ -17,6 +37,11 @@ StructPositiveSum-Safe.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml T StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml TIMEOUT array10_pattern_simplified.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +Acsl01-EnsuresLocal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +Acsl03-EnsuresGlobal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +Tschingelhorn-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT // Unable to decide satisfiability of path constraint array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN From c17b4859eb43731902736026c4e79c4328c0f958 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 12:20:57 +0200 Subject: [PATCH 25/42] Use regex to check if test should be marked as skipped --- .../decider/SafetyCheckTestResultDecider.java | 51 ++++++++++--------- 1 file changed, 26 insertions(+), 25 deletions(-) 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 ce8711eec87..3a58c71f527 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; @@ -89,18 +91,6 @@ public ITestResultEvaluation constructTestResultEval return new SafetyCheckerTestResultEvaluation(); } - private SafetyCheckerOverallResult getOverridenExpectedVerdict() { - if (mOverridenExpectedVerdict == null) { - return null; - } - try { - return SafetyCheckerOverallResult.valueOf(mOverridenExpectedVerdict); - } catch (final IllegalArgumentException e) { - // Cannot convert to SafetyCheckerOverallResult, fall back to provided expected result - return null; - } - } - public class SafetyCheckerTestResultEvaluation implements ITestResultEvaluation { private String mCategory; private String mMessage; @@ -109,10 +99,17 @@ public class SafetyCheckerTestResultEvaluation implements ITestResultEvaluation< @Override public void evaluateTestResult(final IExpectedResultFinder expectedResultFinder, final IOverallResultEvaluator overallResultDeterminer) { - final SafetyCheckerOverallResult expectedVerdict = getOverridenExpectedVerdict(); - if (expectedVerdict != null) { - mMessage = "ExpectedResult (overriden): " + expectedVerdict; - compareToOverallResult(expectedVerdict, overallResultDeterminer, true); + 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); @@ -121,7 +118,7 @@ public void evaluateTestResult(final IExpectedResultFinder overallResultDeterminer, - final boolean skipOnSuccess) { + final IOverallResultEvaluator overallResultDeterminer) { final SafetyCheckerOverallResult overallResult = overallResultDeterminer.getOverallResult(); final String overallResultMsg = overallResultDeterminer.generateOverallResultMessage(); @@ -171,7 +167,7 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes switch (overallResult) { case EXCEPTION_OR_ERROR: mCategory = overallResult + " (Expected:" + expectedResult + ") " + overallResultMsg; - mTestResult = skipOnSuccess && expectedResult == overallResult ? TestResult.IGNORE : TestResult.FAIL; + mTestResult = TestResult.FAIL; break; case SAFE: if (expectedResult == SafetyCheckerOverallResult.SAFE) { @@ -194,7 +190,7 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes break; case UNSAFE_OVERAPPROXIMATED: if (expectedResult == overallResult) { - mTestResult = skipOnSuccess ? TestResult.IGNORE : TestResult.SUCCESS; + mTestResult = TestResult.SUCCESS; } else if (expectedResult == SafetyCheckerOverallResult.UNSAFE) { mTestResult = TestResult.SUCCESS; } else { @@ -210,12 +206,9 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes } break; case UNKNOWN: - case TIMEOUT: // syntax error should always have been found if (expectedResult == SafetyCheckerOverallResult.SYNTAX_ERROR) { mTestResult = TestResult.FAIL; - } else if (skipOnSuccess && expectedResult == overallResult) { - mTestResult = TestResult.IGNORE; } else { mTestResult = TestResult.UNKNOWN; } @@ -227,6 +220,14 @@ private void compareToOverallResult(final SafetyCheckerOverallResult expectedRes mTestResult = TestResult.FAIL; } break; + case TIMEOUT: + // syntax error should always have been found + if (expectedResult == SafetyCheckerOverallResult.SYNTAX_ERROR) { + mTestResult = TestResult.FAIL; + } else { + mTestResult = TestResult.UNKNOWN; + } + break; case UNSUPPORTED_SYNTAX: mTestResult = TestResult.FAIL; break; @@ -293,4 +294,4 @@ public String getTestResultMessage() { return mMessage; } } -} +} \ No newline at end of file From 989a4f2ea778e925bd197a1376db201ab400a0ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 13:14:15 +0200 Subject: [PATCH 26/42] Fix typo --- trunk/examples/concurrent/pthreads/races/regression/.skip | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/trunk/examples/concurrent/pthreads/races/regression/.skip b/trunk/examples/concurrent/pthreads/races/regression/.skip index 6f17d13b14a..97df0a3ea37 100644 --- a/trunk/examples/concurrent/pthreads/races/regression/.skip +++ b/trunk/examples/concurrent/pthreads/races/regression/.skip @@ -4,4 +4,4 @@ static-array-copy3.c DataRace-32bit-Automizer_Default.epf DataRace.xml TIMEOUT static-array-copy3.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml TIMEOUT // Crash in MathSAT -static-array-write.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml EXCEPTION_OR_ERROR +struct-array-write.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml EXCEPTION_OR_ERROR From b72f87889531d6d60a6e6dc7bd7abbe293555336 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 13:21:30 +0200 Subject: [PATCH 27/42] Remove unnecessary .skip file --- trunk/examples/programs/SignedIntegerOverflow/regression/.skip | 3 --- 1 file changed, 3 deletions(-) delete mode 100644 trunk/examples/programs/SignedIntegerOverflow/regression/.skip diff --git a/trunk/examples/programs/SignedIntegerOverflow/regression/.skip b/trunk/examples/programs/SignedIntegerOverflow/regression/.skip deleted file mode 100644 index 6da0e411e33..00000000000 --- a/trunk/examples/programs/SignedIntegerOverflow/regression/.skip +++ /dev/null @@ -1,3 +0,0 @@ -// Fails due to overapproximation of bitwise operators in the integer translation -ShiftLeft06.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml UNKNOWN -ShiftLeft07.c AutomizerC-SignedIntegerOverflowCheck.epf AutomizerC.xml UNKNOWN From b4ea028a7291b0d948a171891ba82064a9b4f536 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 13:36:55 +0200 Subject: [PATCH 28/42] Use YAML for skip files --- .../examples/concurrent/bpl/regression/.skip | 6 --- .../concurrent/bpl/regression/skip.yml | 7 +++ .../pthreads/races/regression/.skip | 7 --- .../pthreads/races/regression/skip.yml | 8 +++ .../concurrent/pthreads/regression/.skip | 2 - .../concurrent/pthreads/regression/skip.yml | 3 ++ .../programs/FloatingPoint/regression/c/.skip | 3 -- .../FloatingPoint/regression/c/skip.yml | 3 ++ .../programs/quantifier/regression/bpl/.skip | 2 - .../quantifier/regression/bpl/skip.yml | 2 + trunk/examples/programs/regression/bpl/.skip | 22 --------- .../examples/programs/regression/bpl/skip.yml | 21 ++++++++ trunk/examples/programs/regression/c/.skip | 48 ------------------ trunk/examples/programs/regression/c/skip.yml | 49 +++++++++++++++++++ .../META-INF/MANIFEST.MF | 3 +- .../AbstractRegressionTestSuite.java | 30 +++++++----- 16 files changed, 112 insertions(+), 104 deletions(-) delete mode 100644 trunk/examples/concurrent/bpl/regression/.skip create mode 100644 trunk/examples/concurrent/bpl/regression/skip.yml delete mode 100644 trunk/examples/concurrent/pthreads/races/regression/.skip create mode 100644 trunk/examples/concurrent/pthreads/races/regression/skip.yml delete mode 100644 trunk/examples/concurrent/pthreads/regression/.skip create mode 100644 trunk/examples/concurrent/pthreads/regression/skip.yml delete mode 100644 trunk/examples/programs/FloatingPoint/regression/c/.skip create mode 100644 trunk/examples/programs/FloatingPoint/regression/c/skip.yml delete mode 100644 trunk/examples/programs/quantifier/regression/bpl/.skip create mode 100644 trunk/examples/programs/quantifier/regression/bpl/skip.yml delete mode 100644 trunk/examples/programs/regression/bpl/.skip create mode 100644 trunk/examples/programs/regression/bpl/skip.yml delete mode 100644 trunk/examples/programs/regression/c/.skip create mode 100644 trunk/examples/programs/regression/c/skip.yml diff --git a/trunk/examples/concurrent/bpl/regression/.skip b/trunk/examples/concurrent/bpl/regression/.skip deleted file mode 100644 index af62a98d004..00000000000 --- a/trunk/examples/concurrent/bpl/regression/.skip +++ /dev/null @@ -1,6 +0,0 @@ -// Timeout with Automizer, GemCutter succeeds -MirabelleConcurrentIncrement.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT -concurrent_increment.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT -equal-array-sums.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT -loop-lockstep-example.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT -sum_invariant.bpl ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT diff --git a/trunk/examples/concurrent/bpl/regression/skip.yml b/trunk/examples/concurrent/bpl/regression/skip.yml new file mode 100644 index 00000000000..feee56c4875 --- /dev/null +++ b/trunk/examples/concurrent/bpl/regression/skip.yml @@ -0,0 +1,7 @@ +# 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 diff --git a/trunk/examples/concurrent/pthreads/races/regression/.skip b/trunk/examples/concurrent/pthreads/races/regression/.skip deleted file mode 100644 index 97df0a3ea37..00000000000 --- a/trunk/examples/concurrent/pthreads/races/regression/.skip +++ /dev/null @@ -1,7 +0,0 @@ -// Timeout -static-array-copy3.c DataRace-32bit-Automizer_Bitvector.epf DataRace.xml TIMEOUT -static-array-copy3.c DataRace-32bit-Automizer_Default.epf DataRace.xml TIMEOUT -static-array-copy3.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml TIMEOUT - -// Crash in MathSAT -struct-array-write.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml EXCEPTION_OR_ERROR diff --git a/trunk/examples/concurrent/pthreads/races/regression/skip.yml b/trunk/examples/concurrent/pthreads/races/regression/skip.yml new file mode 100644 index 00000000000..fc7817d8822 --- /dev/null +++ b/trunk/examples/concurrent/pthreads/races/regression/skip.yml @@ -0,0 +1,8 @@ +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 + +# Crash in MathSAT +SMTLIBException.*mathsat: +- struct-array-write.c DataRace-32bit-GemCutter_Bitvector.epf DataRace.xml \ No newline at end of file diff --git a/trunk/examples/concurrent/pthreads/regression/.skip b/trunk/examples/concurrent/pthreads/regression/.skip deleted file mode 100644 index becc42db31b..00000000000 --- a/trunk/examples/concurrent/pthreads/regression/.skip +++ /dev/null @@ -1,2 +0,0 @@ -// Timeout with Automizer, GemCutter succeeds -NonAtomicIncrement_2Threads.c ReachSafety-32bit-Automizer.epf ReachSafety.xml TIMEOUT diff --git a/trunk/examples/concurrent/pthreads/regression/skip.yml b/trunk/examples/concurrent/pthreads/regression/skip.yml new file mode 100644 index 00000000000..ffab7832c02 --- /dev/null +++ b/trunk/examples/concurrent/pthreads/regression/skip.yml @@ -0,0 +1,3 @@ +# Timeout with Automizer, GemCutter succeeds +TIMEOUT: +- NonAtomicIncrement_2Threads.c ReachSafety-32bit-Automizer.epf ReachSafety.xml diff --git a/trunk/examples/programs/FloatingPoint/regression/c/.skip b/trunk/examples/programs/FloatingPoint/regression/c/.skip deleted file mode 100644 index ecc7d7e059b..00000000000 --- a/trunk/examples/programs/FloatingPoint/regression/c/.skip +++ /dev/null @@ -1,3 +0,0 @@ -// Timeout -SAS09-Float.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml TIMEOUT -ctrans-float-rounding.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml TIMEOUT diff --git a/trunk/examples/programs/FloatingPoint/regression/c/skip.yml b/trunk/examples/programs/FloatingPoint/regression/c/skip.yml new file mode 100644 index 00000000000..88d3dd9e2ab --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/skip.yml @@ -0,0 +1,3 @@ +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 diff --git a/trunk/examples/programs/quantifier/regression/bpl/.skip b/trunk/examples/programs/quantifier/regression/bpl/.skip deleted file mode 100644 index b524850b8a7..00000000000 --- a/trunk/examples/programs/quantifier/regression/bpl/.skip +++ /dev/null @@ -1,2 +0,0 @@ -// Overapproximation -AuxVarInCall.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml UNKNOWN diff --git a/trunk/examples/programs/quantifier/regression/bpl/skip.yml b/trunk/examples/programs/quantifier/regression/bpl/skip.yml new file mode 100644 index 00000000000..fbb692d4ded --- /dev/null +++ b/trunk/examples/programs/quantifier/regression/bpl/skip.yml @@ -0,0 +1,2 @@ +overapproximation: +- AuxVarInCall.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml diff --git a/trunk/examples/programs/regression/bpl/.skip b/trunk/examples/programs/regression/bpl/.skip deleted file mode 100644 index 844306912f7..00000000000 --- a/trunk/examples/programs/regression/bpl/.skip +++ /dev/null @@ -1,22 +0,0 @@ -// Timeout -BugLiveVariables03-Safe.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml TIMEOUT -BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml TIMEOUT -BugNoPredecessorOfReturnTransition.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT -nestedWhileSimple-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT - -// Overapproximation, we expect unknown for Automizer -Overapproximation.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml UNKNOWN -Overapproximation.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml UNKNOWN -Overapproximation.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml UNKNOWN -Overapproximation.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml UNKNOWN - -// The solver is unable to evaluate the formula, PDR cannot handle this -BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml EXCEPTION_OR_ERROR - -// We are unable to backtranslate @diff from SMT to Boogie -BugLiveVariables03-Safe.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml EXCEPTION_OR_ERROR -BugLiveVariables04-Safe.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml EXCEPTION_OR_ERROR - -// Const is only supported for infinite index sort in SMTInterpol -ConstArray.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml EXCEPTION_OR_ERROR -ConstArray.bpl AutomizerBpl-nestedInterpolants.epf PdrAutomizerBpl.xml EXCEPTION_OR_ERROR diff --git a/trunk/examples/programs/regression/bpl/skip.yml b/trunk/examples/programs/regression/bpl/skip.yml new file mode 100644 index 00000000000..576f8330379 --- /dev/null +++ b/trunk/examples/programs/regression/bpl/skip.yml @@ -0,0 +1,21 @@ +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 + +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 + +# 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 + +# 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 diff --git a/trunk/examples/programs/regression/c/.skip b/trunk/examples/programs/regression/c/.skip deleted file mode 100644 index 92cdd01f3ad..00000000000 --- a/trunk/examples/programs/regression/c/.skip +++ /dev/null @@ -1,48 +0,0 @@ -// Fails due to overapproximation of bitwise operators in the integer translation -bitwiseOrUnsigned.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN -bitwiseOrUnsigned.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN -bitwiseOrUnsignedMinimal.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN -builtin_ffs.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN -builtin_ffs.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN -builtin_ffs.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -builtin_ffs.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN -builtin_ffs.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN -builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN -builtin_ffs.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN -BitwiseOperations02.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN -BitwiseOperations02.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN -BitwiseOperations02.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -BitwiseOperations02.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN -BitwiseOperations02.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN -BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN - -// Timeout -BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -BitwiseOperations02.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -ShortCircuit-SideEffect-DoStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -ShortCircuit-SideEffect-ForStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c AutomizerC-forwardPredicates.epf AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml TIMEOUT -array10_pattern_simplified.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -Acsl01-EnsuresLocal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -Acsl03-EnsuresGlobal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT -Tschingelhorn-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT - -// Unable to decide satisfiability of path constraint -array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN -array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN diff --git a/trunk/examples/programs/regression/c/skip.yml b/trunk/examples/programs/regression/c/skip.yml new file mode 100644 index 00000000000..53f204cfb66 --- /dev/null +++ b/trunk/examples/programs/regression/c/skip.yml @@ -0,0 +1,49 @@ +# 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 + +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 + +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 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 09fd5895210..6d4eae8cd6e 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 @@ -26,22 +26,23 @@ */ package de.uni_freiburg.informatik.ultimate.regressiontest; -import java.io.BufferedReader; import java.io.File; import java.io.FileInputStream; -import java.io.IOException; -import java.io.InputStreamReader; +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; @@ -67,7 +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 = ".skip"; + private static final String SKIPPED_FILENAME = "skip.yml"; protected long mTimeout; protected String mRootFolder; @@ -146,17 +147,20 @@ private static NestedMap3 getSkippedTests(final } private static void addSkippedTest(final File ignoreFile, final NestedMap3 map) { - try (BufferedReader br = new BufferedReader(new InputStreamReader(new FileInputStream(ignoreFile)))) { - String line; - while ((line = br.readLine()) != null) { - addSkipLine(line, map); + try { + final Map> parsed = new Yaml().load(new FileInputStream(ignoreFile)); + for (final var entry : parsed.entrySet()) { + for (final String line : entry.getValue()) { + addSkipLine(line, entry.getKey(), map); + } } - } catch (final IOException e) { - // Just skip + } catch (final FileNotFoundException e) { + // File does not exist, nothing to be ignored } } - private static void addSkipLine(final String line, final NestedMap3 map) { + private static void addSkipLine(final String line, final String exptectedVerdict, + final NestedMap3 map) { if (line.startsWith("//")) { return; } @@ -164,7 +168,7 @@ private static void addSkipLine(final String line, final NestedMap3 Date: Tue, 20 Aug 2024 14:58:38 +0200 Subject: [PATCH 29/42] Add missing space --- .../ultimate/test/decider/SafetyCheckTestResultDecider.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 3a58c71f527..1715e61e8ae 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 @@ -108,7 +108,7 @@ public void evaluateTestResult(final IExpectedResultFinder Date: Tue, 20 Aug 2024 15:31:27 +0200 Subject: [PATCH 30/42] Use proper YAML syntax for skip files --- .../concurrent/bpl/regression/skip.yml | 20 +- .../pthreads/races/regression/skip.yml | 16 +- .../concurrent/pthreads/regression/skip.yml | 4 +- .../FloatingPoint/regression/c/skip.yml | 8 +- .../quantifier/regression/bpl/skip.yml | 4 +- .../examples/programs/regression/bpl/skip.yml | 48 +++-- trunk/examples/programs/regression/c/skip.yml | 172 +++++++++++++----- .../AbstractRegressionTestSuite.java | 40 +--- 8 files changed, 207 insertions(+), 105 deletions(-) diff --git a/trunk/examples/concurrent/bpl/regression/skip.yml b/trunk/examples/concurrent/bpl/regression/skip.yml index feee56c4875..10b09b767bc 100644 --- a/trunk/examples/concurrent/bpl/regression/skip.yml +++ b/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 diff --git a/trunk/examples/concurrent/pthreads/races/regression/skip.yml b/trunk/examples/concurrent/pthreads/races/regression/skip.yml index fc7817d8822..a5de3d6a4dd 100644 --- a/trunk/examples/concurrent/pthreads/races/regression/skip.yml +++ b/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 \ No newline at end of file +- task: struct-array-write.c + settings: DataRace-32bit-GemCutter_Bitvector.epf + toolchain: DataRace.xml diff --git a/trunk/examples/concurrent/pthreads/regression/skip.yml b/trunk/examples/concurrent/pthreads/regression/skip.yml index ffab7832c02..f0fe6b28fd3 100644 --- a/trunk/examples/concurrent/pthreads/regression/skip.yml +++ b/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 diff --git a/trunk/examples/programs/FloatingPoint/regression/c/skip.yml b/trunk/examples/programs/FloatingPoint/regression/c/skip.yml index 88d3dd9e2ab..98f261bbceb 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/skip.yml +++ b/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 diff --git a/trunk/examples/programs/quantifier/regression/bpl/skip.yml b/trunk/examples/programs/quantifier/regression/bpl/skip.yml index fbb692d4ded..425385046fb 100644 --- a/trunk/examples/programs/quantifier/regression/bpl/skip.yml +++ b/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 diff --git a/trunk/examples/programs/regression/bpl/skip.yml b/trunk/examples/programs/regression/bpl/skip.yml index 576f8330379..031a706355e 100644 --- a/trunk/examples/programs/regression/bpl/skip.yml +++ b/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 diff --git a/trunk/examples/programs/regression/c/skip.yml b/trunk/examples/programs/regression/c/skip.yml index 53f204cfb66..463e0fba225 100644 --- a/trunk/examples/programs/regression/c/skip.yml +++ b/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 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 6d4eae8cd6e..84e85b801dd 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 @@ -148,10 +148,10 @@ private static NestedMap3 getSkippedTests(final private static void addSkippedTest(final File ignoreFile, final NestedMap3 map) { try { - final Map> parsed = new Yaml().load(new FileInputStream(ignoreFile)); + final Map>> 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 triples : entry.getValue()) { + map.put(triples.get("task"), triples.get("settings"), triples.get("toolchain"), entry.getKey()); } } } catch (final FileNotFoundException e) { @@ -159,40 +159,6 @@ private static void addSkippedTest(final File ignoreFile, final NestedMap3 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; } From 362adb780b8a80cc4cbd30d6fa9442000cedbf23 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 15:59:01 +0200 Subject: [PATCH 31/42] Only allow skip files next to the tests itself --- .../regression/c/{ => noMathSAT}/skip.yml | 0 .../examples/programs/regression/bpl/skip.yml | 9 ----- .../regression/bpl/toolDirectives/skip.yml | 8 +++++ .../regression/c/interprocedural/skip.yml | 10 ++++++ trunk/examples/programs/regression/c/skip.yml | 9 ----- .../AbstractRegressionTestSuite.java | 35 ++++++++++--------- 6 files changed, 36 insertions(+), 35 deletions(-) rename trunk/examples/programs/FloatingPoint/regression/c/{ => noMathSAT}/skip.yml (100%) create mode 100644 trunk/examples/programs/regression/bpl/toolDirectives/skip.yml create mode 100644 trunk/examples/programs/regression/c/interprocedural/skip.yml diff --git a/trunk/examples/programs/FloatingPoint/regression/c/skip.yml b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/skip.yml similarity index 100% rename from trunk/examples/programs/FloatingPoint/regression/c/skip.yml rename to trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/skip.yml diff --git a/trunk/examples/programs/regression/bpl/skip.yml b/trunk/examples/programs/regression/bpl/skip.yml index 031a706355e..b241000ef13 100644 --- a/trunk/examples/programs/regression/bpl/skip.yml +++ b/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 diff --git a/trunk/examples/programs/regression/bpl/toolDirectives/skip.yml b/trunk/examples/programs/regression/bpl/toolDirectives/skip.yml new file mode 100644 index 00000000000..d79a7d11335 --- /dev/null +++ b/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 diff --git a/trunk/examples/programs/regression/c/interprocedural/skip.yml b/trunk/examples/programs/regression/c/interprocedural/skip.yml new file mode 100644 index 00000000000..78b3932a404 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/trunk/examples/programs/regression/c/skip.yml b/trunk/examples/programs/regression/c/skip.yml index 463e0fba225..9f91edc0a51 100644 --- a/trunk/examples/programs/regression/c/skip.yml +++ b/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 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 84e85b801dd..f232fbfb590 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 @@ -117,12 +117,12 @@ public Collection createTestCases() { final Predicate filesRegexFilter = getFilesRegexFilter(); for (final Config runConfiguration : runConfigurations) { final Collection inputFiles = getInputFiles(filesRegexFilter, runConfiguration); - final NestedMap3 skippedTests = getSkippedTests(runConfiguration); + final NestedMap3 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))); } @@ -130,28 +130,29 @@ public Collection createTestCases() { return rtr; } - private static NestedMap3 getSkippedTests(final Config runConfiguration) { - final NestedMap3 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 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) { + 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()) { - 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) { From a782a21a35a56241b1b3199639e4ca19716953f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Mon, 2 Sep 2024 10:09:37 +0200 Subject: [PATCH 32/42] Use .testignore as filename --- .../concurrent/bpl/regression/{skip.yml => .testignore} | 0 .../pthreads/races/regression/{skip.yml => .testignore} | 0 .../concurrent/pthreads/regression/{skip.yml => .testignore} | 0 .../regression/c/noMathSAT/{skip.yml => .testignore} | 0 .../quantifier/regression/bpl/{skip.yml => .testignore} | 0 .../examples/programs/regression/bpl/{skip.yml => .testignore} | 0 .../regression/bpl/toolDirectives/{skip.yml => .testignore} | 0 trunk/examples/programs/regression/c/{skip.yml => .testignore} | 0 .../regression/c/interprocedural/{skip.yml => .testignore} | 0 .../ultimate/regressiontest/AbstractRegressionTestSuite.java | 2 +- 10 files changed, 1 insertion(+), 1 deletion(-) rename trunk/examples/concurrent/bpl/regression/{skip.yml => .testignore} (100%) rename trunk/examples/concurrent/pthreads/races/regression/{skip.yml => .testignore} (100%) rename trunk/examples/concurrent/pthreads/regression/{skip.yml => .testignore} (100%) rename trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/{skip.yml => .testignore} (100%) rename trunk/examples/programs/quantifier/regression/bpl/{skip.yml => .testignore} (100%) rename trunk/examples/programs/regression/bpl/{skip.yml => .testignore} (100%) rename trunk/examples/programs/regression/bpl/toolDirectives/{skip.yml => .testignore} (100%) rename trunk/examples/programs/regression/c/{skip.yml => .testignore} (100%) rename trunk/examples/programs/regression/c/interprocedural/{skip.yml => .testignore} (100%) diff --git a/trunk/examples/concurrent/bpl/regression/skip.yml b/trunk/examples/concurrent/bpl/regression/.testignore similarity index 100% rename from trunk/examples/concurrent/bpl/regression/skip.yml rename to trunk/examples/concurrent/bpl/regression/.testignore diff --git a/trunk/examples/concurrent/pthreads/races/regression/skip.yml b/trunk/examples/concurrent/pthreads/races/regression/.testignore similarity index 100% rename from trunk/examples/concurrent/pthreads/races/regression/skip.yml rename to trunk/examples/concurrent/pthreads/races/regression/.testignore diff --git a/trunk/examples/concurrent/pthreads/regression/skip.yml b/trunk/examples/concurrent/pthreads/regression/.testignore similarity index 100% rename from trunk/examples/concurrent/pthreads/regression/skip.yml rename to trunk/examples/concurrent/pthreads/regression/.testignore diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/skip.yml b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore similarity index 100% rename from trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/skip.yml rename to trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore diff --git a/trunk/examples/programs/quantifier/regression/bpl/skip.yml b/trunk/examples/programs/quantifier/regression/bpl/.testignore similarity index 100% rename from trunk/examples/programs/quantifier/regression/bpl/skip.yml rename to trunk/examples/programs/quantifier/regression/bpl/.testignore diff --git a/trunk/examples/programs/regression/bpl/skip.yml b/trunk/examples/programs/regression/bpl/.testignore similarity index 100% rename from trunk/examples/programs/regression/bpl/skip.yml rename to trunk/examples/programs/regression/bpl/.testignore diff --git a/trunk/examples/programs/regression/bpl/toolDirectives/skip.yml b/trunk/examples/programs/regression/bpl/toolDirectives/.testignore similarity index 100% rename from trunk/examples/programs/regression/bpl/toolDirectives/skip.yml rename to trunk/examples/programs/regression/bpl/toolDirectives/.testignore diff --git a/trunk/examples/programs/regression/c/skip.yml b/trunk/examples/programs/regression/c/.testignore similarity index 100% rename from trunk/examples/programs/regression/c/skip.yml rename to trunk/examples/programs/regression/c/.testignore diff --git a/trunk/examples/programs/regression/c/interprocedural/skip.yml b/trunk/examples/programs/regression/c/interprocedural/.testignore similarity index 100% rename from trunk/examples/programs/regression/c/interprocedural/skip.yml rename to trunk/examples/programs/regression/c/interprocedural/.testignore 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 f232fbfb590..d3b20f1a139 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 @@ -68,7 +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 = "skip.yml"; + private static final String SKIPPED_FILENAME = ".testignore"; protected long mTimeout; protected String mRootFolder; From 594d1155be907d97b9972708f76d8d760d52ecd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 3 Sep 2024 12:29:00 +0200 Subject: [PATCH 33/42] Split .testignore properly for subfolders --- .../programs/regression/bpl/.testignore | 32 ------------------- .../bpl/interprocedural/.testignore | 16 ++++++++++ .../regression/bpl/toolDirectives/.testignore | 17 ++++++++++ 3 files changed, 33 insertions(+), 32 deletions(-) create mode 100644 trunk/examples/programs/regression/bpl/interprocedural/.testignore diff --git a/trunk/examples/programs/regression/bpl/.testignore b/trunk/examples/programs/regression/bpl/.testignore index b241000ef13..0e6d1d6de5b 100644 --- a/trunk/examples/programs/regression/bpl/.testignore +++ b/trunk/examples/programs/regression/bpl/.testignore @@ -1,36 +1,4 @@ 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 - task: nestedWhileSimple-Safe.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 - -# 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/interprocedural/.testignore b/trunk/examples/programs/regression/bpl/interprocedural/.testignore new file mode 100644 index 00000000000..ecda10a8bb3 --- /dev/null +++ b/trunk/examples/programs/regression/bpl/interprocedural/.testignore @@ -0,0 +1,16 @@ +TIMEOUT: +- task: BugLiveVariables03-Safe.bpl + settings: AutomizerBpl-FPandBP.epf + toolchain: AutomizerBpl.xml +- task: BugNestedSsaWithPendingContexts.bpl + settings: AutomizerBpl-forwardPredicates.epf + toolchain: AutomizerBpl.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 index d79a7d11335..ad375761f78 100644 --- a/trunk/examples/programs/regression/bpl/toolDirectives/.testignore +++ b/trunk/examples/programs/regression/bpl/toolDirectives/.testignore @@ -6,3 +6,20 @@ Const is only supported for infinite index sort: - 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 From f845e42c1f17de56352c5f4d127d766463fb163d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 3 Sep 2024 12:40:09 +0200 Subject: [PATCH 34/42] Allow skipping termination tests --- trunk/examples/lassos/regression/.testignore | 5 +++++ .../TerminationAnalysisTestResultDecider.java | 18 ++++++++++++++++++ 2 files changed, 23 insertions(+) create mode 100644 trunk/examples/lassos/regression/.testignore 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/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..fce351f8154 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 @@ -50,6 +50,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 +84,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: From 261c3fa0d1465aad5c70e461304f61d23270c180 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 3 Sep 2024 12:48:07 +0200 Subject: [PATCH 35/42] Add missing import --- .../test/decider/TerminationAnalysisTestResultDecider.java | 2 ++ 1 file changed, 2 insertions(+) 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 fce351f8154..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; From 10f0efb87fca5f969a23bc0c044cde993ca142af Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 3 Sep 2024 12:49:20 +0200 Subject: [PATCH 36/42] Add newline --- .../ultimate/test/decider/SafetyCheckTestResultDecider.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 1715e61e8ae..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 @@ -294,4 +294,4 @@ public String getTestResultMessage() { return mMessage; } } -} \ No newline at end of file +} From 1fbf05f7d5432d108c3c113b5b302aa5a8007651 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 3 Sep 2024 12:54:32 +0200 Subject: [PATCH 37/42] Add checks for no overriden result --- .../translation/C2BoogieRegressionTestSuite.java | 4 +++- .../translation/LTLTranslationRegressionTestSuite.java | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java index c3cf516d455..4bd7f3d42c0 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java @@ -66,7 +66,9 @@ public C2BoogieRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + checkNoOverridenVerdict(overridenExpectedVerdict); return new TranslationTestResultDecider(runDefinition.selectPrimaryInputFile()); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java index 63f282d019b..4a6a36d21c3 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java @@ -48,7 +48,9 @@ public LTLTranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, String overridenExpectedVerdict) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + checkNoOverridenVerdict(overridenExpectedVerdict); return new TranslationTestResultDecider(runDefinition.selectPrimaryInputFile()); } From 9a97c39b9306b0c458e22c262bd5c7467392992d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 3 Sep 2024 12:55:41 +0200 Subject: [PATCH 38/42] Add newline --- .../examples/programs/regression/c/interprocedural/.testignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/trunk/examples/programs/regression/c/interprocedural/.testignore b/trunk/examples/programs/regression/c/interprocedural/.testignore index 78b3932a404..623f87ba48e 100644 --- a/trunk/examples/programs/regression/c/interprocedural/.testignore +++ b/trunk/examples/programs/regression/c/interprocedural/.testignore @@ -7,4 +7,4 @@ TIMEOUT: toolchain: AutomizerC.xml - task: Tschingelhorn-Safe.c settings: AutomizerC-BitvectorTranslation.epf - toolchain: AutomizerC.xml \ No newline at end of file + toolchain: AutomizerC.xml From 1f5cc6af05eff1507680035923ba1aede1b4826b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Wed, 4 Sep 2024 10:15:24 +0200 Subject: [PATCH 39/42] Avoid parentheses in regex --- .../programs/regression/bpl/interprocedural/.testignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/trunk/examples/programs/regression/bpl/interprocedural/.testignore b/trunk/examples/programs/regression/bpl/interprocedural/.testignore index ecda10a8bb3..74aa8730e30 100644 --- a/trunk/examples/programs/regression/bpl/interprocedural/.testignore +++ b/trunk/examples/programs/regression/bpl/interprocedural/.testignore @@ -7,7 +7,7 @@ TIMEOUT: toolchain: AutomizerBpl.xml # We are unable to backtranslate @diff from SMT to Boogie -unknown symbol (@diff: +unknown symbol.*@diff: - task: BugLiveVariables03-Safe.bpl settings: AutomizerBpl-nestedInterpolants.epf toolchain: AutomizerBpl.xml From c9d2c0b01924a6eaaf5778aa7b0bcdb98bc7a3b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Wed, 4 Sep 2024 10:21:00 +0200 Subject: [PATCH 40/42] Add timeout --- .../programs/regression/bpl/interprocedural/.testignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/trunk/examples/programs/regression/bpl/interprocedural/.testignore b/trunk/examples/programs/regression/bpl/interprocedural/.testignore index 74aa8730e30..0680edba95a 100644 --- a/trunk/examples/programs/regression/bpl/interprocedural/.testignore +++ b/trunk/examples/programs/regression/bpl/interprocedural/.testignore @@ -5,6 +5,9 @@ TIMEOUT: - 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: From 95ffcc8b346717b4cc4fe164c9e804ecba14e053 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Wed, 4 Sep 2024 10:21:20 +0200 Subject: [PATCH 41/42] Skip termination tests properly --- .../regressiontest/generic/TerminationRegressionTestSuite.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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 541263435ee..fd67dc2b697 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 @@ -52,8 +52,7 @@ public TerminationRegressionTestSuite() { @Override protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); - return new TerminationAnalysisTestResultDecider(runDefinition, false); + return new TerminationAnalysisTestResultDecider(runDefinition, false, overridenExpectedVerdict); } } From ecb5fa7876829d3a1b651e8e0ecc29587e4f8f6d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Mon, 9 Sep 2024 12:52:09 +0200 Subject: [PATCH 42/42] Add separate method to override verdict --- .../AbstractRegressionTestSuite.java | 14 +++++++------- .../BoogieBacktranslationRegressionTestSuite.java | 4 +--- .../CBacktranslationRegressionTestSuite.java | 4 +--- .../generic/AbsIntRegressionTestSuite.java | 4 +--- .../AutomataLibraryRegressionTestSuite.java | 4 +--- .../generic/ChcRegressionTestSuite.java | 8 +++----- .../generic/DataRaceRegressionTestSuite.java | 5 +++++ .../generic/LTLRegressionTestSuite.java | 4 +--- .../generic/MSODRegressionTestSuite.java | 4 +--- .../generic/RegressionTestSuite.java | 5 +++++ .../ReqCheckerRedundancyRegressionTestSuite.java | 4 +--- .../generic/ReqCheckerRegressionTestSuite.java | 4 +--- .../SignedIntegerOverflowRegressionTestSuite.java | 5 +++++ .../generic/TerminationRegressionTestSuite.java | 5 +++++ .../generic/WitnessRegressionTestSuite.java | 6 ++---- .../translation/C2BoogieRegressionTestSuite.java | 4 +--- .../LTLTranslationRegressionTestSuite.java | 4 +--- 17 files changed, 42 insertions(+), 46 deletions(-) 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 d3b20f1a139..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 @@ -124,7 +124,9 @@ public Collection createTestCases() { runConfiguration.getToolchainFile(), getTimeout(runConfiguration, inputFile)); final String overridenVerdict = skippedTests.get(inputFile, runConfiguration.getSettingsFile().getName(), runConfiguration.getToolchainFile().getName()); - rtr.add(buildTestCase(urd, getTestResultDecider(urd, overridenVerdict))); + final ITestResultDecider decider = overridenVerdict == null ? getTestResultDecider(urd) + : getTestResultDecider(urd, overridenVerdict); + rtr.add(buildTestCase(urd, decider)); } } return rtr; @@ -303,13 +305,11 @@ protected Collection getInputFiles(final Predicate regexFilter, fina .collect(Collectors.toList()); } - protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition, - String overridenExpectedVerdict); + protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition); - protected void checkNoOverridenVerdict(final String overridenExpectedVerdict) { - if (overridenExpectedVerdict != null) { - throw new UnsupportedOperationException(getClass().getSimpleName() + " does not support skipping tests."); - } + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + throw new UnsupportedOperationException(getClass().getSimpleName() + " does not support skipping tests."); } public static final class Config diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java index 7457bdb0491..8b718651698 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/BoogieBacktranslationRegressionTestSuite.java @@ -46,9 +46,7 @@ public BoogieBacktranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new BacktranslationTestResultDecider(runDefinition); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java index 6a53cab2a53..26d4db005c7 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/backtranslation/CBacktranslationRegressionTestSuite.java @@ -46,9 +46,7 @@ public CBacktranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new BacktranslationTestResultDecider(runDefinition); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java index 58e298a6180..fb6bf240826 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AbsIntRegressionTestSuite.java @@ -51,9 +51,7 @@ public AbsIntRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new OverapproximatingSafetyCheckTestResultDecider(runDefinition, true); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java index 71043cb1e99..c167bca53d5 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/AutomataLibraryRegressionTestSuite.java @@ -50,9 +50,7 @@ public AutomataLibraryRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new AutomataScriptTestResultDecider(); } 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 a3ef71342b0..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,15 +51,13 @@ 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, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { 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 b2312669680..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 @@ -45,6 +45,11 @@ public DataRaceRegressionTestSuite() { mFiletypesToConsider = new String[] { FILE_ENDING }; } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + return new SafetyCheckTestResultDecider(runDefinition, false); + } + @Override protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final String overridenExpectedVerdict) { diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java index 63697973ced..2bae9b85ab4 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/LTLRegressionTestSuite.java @@ -49,9 +49,7 @@ public LTLRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new LTLCheckerTestResultDecider(runDefinition, false); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java index cde8e97e7bc..5118211951d 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/MSODRegressionTestSuite.java @@ -51,9 +51,7 @@ public MSODRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { final boolean unknownIsSuccess = true; return new MSODTestResultDecider(runDefinition, unknownIsSuccess); } 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 ef50d57a715..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 @@ -53,6 +53,11 @@ public RegressionTestSuite() { ".*(CToBoogieTranslation|Backtranslation|lassos|termination|SignedIntegerOverflow|abstractInterpretation|Automata|LTL|DataRace|witness-checking).*"; } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + return new SafetyCheckTestResultDecider(runDefinition, false); + } + @Override protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final String 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 4849dad0506..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 @@ -76,9 +76,7 @@ public ReqCheckerRedundancyRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new ReqCheckerTestResultDecider(runDefinition, false); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java index 4032ec22066..7c74c33fcab 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRegressionTestSuite.java @@ -79,9 +79,7 @@ public ReqCheckerRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new ReqCheckerTestResultDecider(runDefinition, false); } 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 996a4548d76..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 @@ -47,6 +47,11 @@ public SignedIntegerOverflowRegressionTestSuite() { mRootFolder = TestUtil.getPathFromTrunk("examples/programs/SignedIntegerOverflow/"); } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + return new SafetyCheckTestResultDecider(runDefinition, false); + } + @Override protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final String 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 fd67dc2b697..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 @@ -49,6 +49,11 @@ public TerminationRegressionTestSuite() { mIncludeFilterRegexToolchain = ".*(lassos|termination).*"; } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + return new TerminationAnalysisTestResultDecider(runDefinition, false); + } + @Override protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, final String overridenExpectedVerdict) { diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java index c0a8a3d6cf4..1d5d85f033c 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java @@ -61,9 +61,7 @@ public WitnessRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new WitnessSafetyCheckTestResultDecider(runDefinition); } @@ -79,7 +77,7 @@ public Collection createTestCases() { final File[] newFiles = DataStructureUtils.concat(def.getInput(), new File[] { witness }); final UltimateRunDefinition newDef = new UltimateRunDefinition(newFiles, def.getSettings(), def.getToolchain(), def.getTimeout()); - result.add(new UltimateTestCase(getTestResultDecider(def, null), newDef, List.of(), null)); + result.add(new UltimateTestCase(getTestResultDecider(def), newDef, List.of(), null)); } } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java index 4bd7f3d42c0..e1eafac9941 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/C2BoogieRegressionTestSuite.java @@ -66,9 +66,7 @@ public C2BoogieRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new TranslationTestResultDecider(runDefinition.selectPrimaryInputFile()); } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java index 4a6a36d21c3..4ae4a304130 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/translation/LTLTranslationRegressionTestSuite.java @@ -48,9 +48,7 @@ public LTLTranslationRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, - final String overridenExpectedVerdict) { - checkNoOverridenVerdict(overridenExpectedVerdict); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { return new TranslationTestResultDecider(runDefinition.selectPrimaryInputFile()); }