add comments

Author: d367wang

testdata/ostrusted-unsat-test/Unsat.java

@@ -1,6 +1,13 @@
 import ostrusted.qual.OsUntrusted;
 import ostrusted.qual.OsTrusted;
 
+/**
+ * This case is unsatisfiable, because in method {@code m()},
+ * <p>(1) at line 18, the local variable {@code s} is refined by the return type of {@code bar()}.
+ *     Denote the refinement variable as @1, then @1 == @OsUntrusted.
+ * <p>(2) at line 20, {@code s} is passed to method {@code foo} as the argument, therefore @1 <: @OsTrusted
+ *     since @OsTrusted is bottom, @1 == @OsTrusted.
+ */
 class Unsat {
 
     void foo(@OsTrusted String s) {}

tests/checkers/inference/test/CFInferenceTest.java

@@ -60,6 +60,11 @@ testFile, testDataDir, checkerName, checkerOptions, getAdditionalInferenceOption
         postProcessResult(testResult);
     }
 
+    /**
+     * Report a summary of the failed test based on the {@link InferenceTestResult}.
+     *
+     * @param testResult the test result returned by {@code InferenceTestExecutor}
+     */
     protected void postProcessResult(InferenceTestResult testResult) {
         InferenceTestUtilities.assertResultsAreValid(testResult);
     }

tests/checkers/inference/test/CFInferenceUnsatTest.java

@@ -6,8 +6,9 @@
 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.
+ * This test suite runs inference individually on target files that are unsatisfiable. A test case passes
+ * when it passes the initial check phase (i.e. outputs expected errors/warnings and none unexpected ones),
+ * while fails at the inference phase and then terminates.
  *
  * 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.