Report AlwaysFalseConstraints as CF errors

testdata/ostrusted-unsat-test/Unsat.java

@@ -0,0 +1,16 @@
+import ostrusted.qual.OsUntrusted;
+import ostrusted.qual.OsTrusted;
+
+class Unsat {
+
+    void foo(@OsTrusted String s) {}
+
+    @OsUntrusted
+    String bar() { return ""; }
+
+    void m() {
+        String s = bar();
+        // :: error: (argument.type.incompatible)
+        foo(s);
+    }
+}

tests/checkers/inference/OsTrustedUnsatTest.java

@@ -0,0 +1,31 @@
+package checkers.inference;
+
+import checkers.inference.solver.SolverEngine;
+import checkers.inference.test.CFInferenceUnsatTest;
+import org.checkerframework.framework.test.TestUtilities;
+import org.checkerframework.javacutil.Pair;
+import org.junit.runners.Parameterized;
+
+import java.io.File;
+import java.util.ArrayList;
+import java.util.List;
+
+public class OsTrustedUnsatTest extends CFInferenceUnsatTest {
+
+    public OsTrustedUnsatTest(File testFile) {
+        super(testFile,  ostrusted.OsTrustedChecker.class, "ostrusted",
+                "-Anomsgtext",  "-Astubs=src/ostrusted/jdk.astub", "-d", "tests/build/outputdir");
+    }
+
+    @Override
+    public Pair<String, List<String>> getSolverNameAndOptions() {
+        return Pair.<String, List<String>>of(SolverEngine.class.getCanonicalName(), new ArrayList<String>());
+    }
+
+    @Parameterized.Parameters
+    public static List<File> getTestFiles(){
+        List<File> testfiles = new ArrayList<>();//InferenceTestUtilities.findAllSystemTests();
+        testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testdata", "ostrusted-unsat-test"));
+        return testfiles;
+    }
+}

tests/checkers/inference/test/CFInferenceTest.java

@@ -57,6 +57,10 @@ testFile, testDataDir, checkerName, checkerOptions, getAdditionalInferenceOption
                 solverArgs.second, useHacks(), shouldEmitDebugInfo, getPathToAfuScripts(), getPathToInferenceScript());
 
         InferenceTestResult testResult = new InferenceTestExecutor().runTest(config);
+        postProcessResult(testResult);
+    }
+
+    protected void postProcessResult(InferenceTestResult testResult) {
         InferenceTestUtilities.assertResultsAreValid(testResult);
     }
 }

tests/checkers/inference/test/CFInferenceUnsatTest.java

@@ -0,0 +1,33 @@
+package checkers.inference.test;
+
+import org.checkerframework.javacutil.SystemUtil;
+
+import javax.annotation.processing.AbstractProcessor;
+import java.io.File;
+
+/**
+ * This test suite runs inference individually on target files that are unsatisfiable. This means each
+ * test case is expected to pass the initial check phase while fail at the inference phase and terminate.
+ *
+ * The use of this class is the same as {@link CFInferenceTest}. Note that the target directory of the test
+ * cases can only contain unsatisfiable cases.
+ */
+public abstract class CFInferenceUnsatTest extends CFInferenceTest{
+    public CFInferenceUnsatTest(File testFile, Class<? extends AbstractProcessor> checker,
+                           String testDir, String... checkerOptions) {
+        super(testFile, checker, testDir, checkerOptions);
+    }
+
+    @Override
+    protected void postProcessResult(InferenceTestResult testResult) {
+        final InferenceTestPhase lastPhaseRun = testResult.getLastPhaseRun();
+        if (lastPhaseRun == InferenceTestPhase.INITIAL_TYPECHECK) {
+            InferenceTestUtilities.assertResultsAreValid(testResult);
+
+        } else if (lastPhaseRun == InferenceTestPhase.FINAL_TYPECHECK) {
+            String summary = "Inference is expected to fail, but succeeded on source files: \n"
+                    + SystemUtil.join("\n", testResult.getConfiguration().getInitialTypecheckConfig().getTestSourceFiles()) + "\n\n";
+            InferenceTestUtilities.assertFail(InferenceTestPhase.INFER, summary);
+        }
+    }
+}