Skip to content

Commit

Permalink
Skip data race tests
Browse files Browse the repository at this point in the history
  • Loading branch information
schuessf committed Aug 20, 2024
1 parent b5508be commit d43de7f
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 22 deletions.
7 changes: 7 additions & 0 deletions trunk/examples/concurrent/pthreads/races/regression/.skip
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
Expand Up @@ -26,49 +26,28 @@
*/
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 {

private static final int TIMEOUT = 20_000;
private static final String ROOT_DIR = TestUtil.getPathFromTrunk("examples/concurrent/pthreads/races");
private static final String FILE_ENDING = ".c";

private final Map<Pair<String, String>, 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);
}
}

0 comments on commit d43de7f

Please sign in to comment.