From e53cefee0df98f9a080e2a8b79b4533979bdeaf3 Mon Sep 17 00:00:00 2001 From: Tianrui Zheng Date: Tue, 19 Nov 2024 16:22:36 +0100 Subject: [PATCH] Change 3 results in C11LFDSTest and override getConfiguration() Signed-off-by: Tianrui Zheng --- .../java/com/dat3m/dartagnan/c/C11LFDSTest.java | 13 ++++++++++--- .../java/com/dat3m/dartagnan/c/VMMLFDSTest.java | 7 +++++++ 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java index dedd9fc567..d2dafa7aca 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java @@ -10,6 +10,8 @@ import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import java.io.IOException; @@ -27,6 +29,11 @@ public C11LFDSTest(String name, Arch target, Result expected) { super(name, target, expected); } + @Override + protected Configuration getConfiguration() throws InvalidConfigurationException { + return Configuration.defaultConfiguration(); + } + @Override protected Provider getProgramPathProvider() { return () -> getTestResourcePath("lfds/" + name + ".ll"); @@ -55,11 +62,11 @@ protected Provider getSolverProvider() { public static Iterable data() throws IOException { // Commented ones take too long ATM return Arrays.asList(new Object[][]{ - {"dglm", C11, UNKNOWN}, + {"dglm", C11, FAIL}, {"dglm-CAS-relaxed", C11, FAIL}, - {"ms", C11, UNKNOWN}, + {"ms", C11, FAIL}, {"ms-CAS-relaxed", C11, FAIL}, - {"treiber", C11, UNKNOWN}, + {"treiber", C11, FAIL}, {"treiber-CAS-relaxed", C11, FAIL}, {"chase-lev", C11, PASS}, // These have an extra thief that violate the assertion diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLFDSTest.java index bd6818f75e..9566fa7bde 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLFDSTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/VMMLFDSTest.java @@ -10,6 +10,8 @@ import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import java.io.IOException; @@ -29,6 +31,11 @@ public VMMLFDSTest(String name, Arch target, Result expected) { super(name, target, expected); } + @Override + protected Configuration getConfiguration() throws InvalidConfigurationException { + return Configuration.defaultConfiguration(); + } + @Override protected Provider getProgramPathProvider() { return () -> getTestResourcePath("lfds/" + name + ".ll");