From d43de7fd91c89aef0b0d39598ce7930e998c4eaa 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] 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); } }