Boolean variables in dataflow

checker/tests/nullness/Issue406.java

@@ -0,0 +1,58 @@
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class Issue406 {
+  static class LocalDate {}
+
+  private void testFails1(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean eitherIsNull = x1 == null || x2 == null;
+    if (eitherIsNull) return;
+    delegate(x1, x2);
+  }
+
+  private void testFails1b(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean eitherIsNull = x1 == null || x2 == null;
+    if (!eitherIsNull) {
+      delegate(x1, x2);
+    }
+  }
+
+  private void testFails2(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean firstIsNull = x1 == null;
+    boolean secondIsNull = x2 == null;
+    if (firstIsNull || secondIsNull) return;
+    delegate(x1, x2);
+  }
+
+  private void testFails2b(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean firstIsNull = x1 == null;
+    boolean secondIsNull = x2 == null;
+    if (!firstIsNull) {
+      @NonNull LocalDate z = x1;
+    }
+
+    if (firstIsNull || secondIsNull) return;
+    delegate(x1, x2);
+  }
+
+  private void test3(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean firstIsNull = x1 != null;
+    boolean secondIsNull = x2 != null;
+    if (!firstIsNull || !secondIsNull) {
+      // ::  error: (argument)
+      delegate(
+          x1,
+          // ::  error: (argument)
+          x2);
+    }
+  }
+
+  private void testWorks(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    if (x1 == null || x2 == null) return;
+    delegate(x1, x2);
+  }
+
+  private void delegate(LocalDate x1, LocalDate x2) {
+    // do something
+  }
+}

checker/tests/optional/OptionalBooleanVariableFlowRefinement.java

@@ -0,0 +1,36 @@
+import java.util.List;
+import java.util.Optional;
+import org.checkerframework.checker.optional.qual.*;
+import org.checkerframework.dataflow.qual.*;
+
+@SuppressWarnings({"optional:parameter", "optional:field", "optional:collection"})
+class OptionalBooleanVariableFlowRefinement {
+
+  void validRefinementTest(Optional<String> opt) {
+    boolean optIsPresent = opt.isPresent();
+    if (optIsPresent) {
+      opt.get(); // Legal
+    }
+  }
+
+  void otherValidRefinement(OptContainer container) {
+    boolean isGetLegal =
+        container.getOptStrs().isPresent() && !container.getOptStrs().get().isEmpty();
+    if (isGetLegal) {
+      container.getOptStrs().get(); // Legal
+    }
+  }
+
+  class OptContainer {
+    private Optional<List<String>> strs;
+
+    public OptContainer(List<String> strs) {
+      this.strs = Optional.ofNullable(strs);
+    }
+
+    @Pure
+    public Optional<List<String>> getOptStrs() {
+      return this.strs;
+    }
+  }
+}

checker/tests/resourceleak/DaikonFail.java

@@ -0,0 +1,37 @@
+import java.io.File;
+import java.io.PrintStream;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class DaikonFail {
+
+  public static @Nullable File generate_goals = null;
+  public static File diff_file = new File("InvariantFormatTest.diffs");
+
+  private boolean execute() {
+
+    boolean result = performTest();
+
+    if (generate_goals != null) {
+      try {
+        PrintStream out_fp = new PrintStream(generate_goals);
+        out_fp.close();
+      } catch (Exception e) {
+        throw new RuntimeException();
+      }
+    } else {
+      if (!result) {
+        try {
+          PrintStream diff_fp = new PrintStream(diff_file);
+          diff_fp.close();
+        } catch (Exception e) {
+        }
+        return false;
+      }
+    }
+    return true;
+  }
+
+  private boolean performTest() {
+    return false;
+  }
+}