Added tests for the IFlow SAT solvers.

typetools · Oct 15, 2015 · 2cdf7bc · 2cdf7bc
1 parent 3baf870
commit 2cdf7bc
Show file tree

Hide file tree

Showing 2 changed files with 66 additions and 0 deletions.
diff --git a/tests/checkers/inference/IFlowSinkSatTest.java b/tests/checkers/inference/IFlowSinkSatTest.java
@@ -0,0 +1,33 @@
+package checkers.inference;
+
+import checkers.inference.test.CFInferenceTest;
+import org.checkerframework.framework.test.TestUtilities;
+import org.checkerframework.javacutil.Pair;
+import org.junit.runners.Parameterized.Parameters;
+import sparta.checkers.IFlowSinkChecker;
+import sparta.checkers.sat.SinkSolver;
+
+import java.io.File;
+import java.util.ArrayList;
+import java.util.List;
+
+public class IFlowSinkSatTest extends CFInferenceTest {
+
+    public IFlowSinkSatTest(File testFile) {
+        super(testFile,  IFlowSinkChecker.class, "sparta"+File.separator+"checkers",
+                "-Anomsgtext",  "-Astubs=src/sparta/checkers/information_flow.astub", "-d", "tests/build/outputdir");
+    }
+
+    @Override
+    public Pair<String, List<String>> getSolverNameAndOptions() {
+        return Pair.<String, List<String>>of(SinkSolver.class.getCanonicalName(), new ArrayList<String>());
+    }
+
+    @Parameters
+    public static List<File> getTestFiles(){
+        List<File> testfiles = new ArrayList<>();//InferenceTestUtilities.findAllSystemTests();
+        TestUtilities.filterOutJdk8Sources(testfiles);
+        testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testdata", "iflowsink"));
+        return testfiles;
+    }
+}
diff --git a/tests/checkers/inference/IFlowSourceSatTest.java b/tests/checkers/inference/IFlowSourceSatTest.java
@@ -0,0 +1,33 @@
+package checkers.inference;
+
+import checkers.inference.test.CFInferenceTest;
+import org.checkerframework.framework.test.TestUtilities;
+import org.checkerframework.javacutil.Pair;
+import org.junit.runners.Parameterized.Parameters;
+import sparta.checkers.IFlowSourceChecker;
+import sparta.checkers.sat.SourceSolver;
+
+import java.io.File;
+import java.util.ArrayList;
+import java.util.List;
+
+public class IFlowSourceSatTest extends CFInferenceTest {
+
+    public IFlowSourceSatTest(File testFile) {
+        super(testFile,  IFlowSourceChecker.class, "sparta"+File.separator+"checkers",
+                "-Anomsgtext",  "-Astubs=src/sparta/checkers/information_flow.astub", "-d", "tests/build/outputdir");
+    }
+
+    @Override
+    public Pair<String, List<String>> getSolverNameAndOptions() {
+        return Pair.<String, List<String>>of(SourceSolver.class.getCanonicalName(), new ArrayList<String>());
+    }
+
+    @Parameters
+    public static List<File> getTestFiles(){
+        List<File> testfiles = new ArrayList<>();//InferenceTestUtilities.findAllSystemTests();
+        TestUtilities.filterOutJdk8Sources(testfiles);
+        testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testdata", "iflowsource"));
+        return testfiles;
+    }
+}