False positive.

typetools · Dec 4, 2024 · ba3ccd4 · ba3ccd4
1 parent 1ba21ef
commit ba3ccd4
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 4 deletions.
diff --git a/checker/tests/nonempty/SizeInIsEmpty.java b/checker/tests/nonempty/SizeInIsEmpty.java
@@ -1,5 +1,7 @@
 import java.util.AbstractSet;
+import java.util.HashSet;
 import java.util.Iterator;
+import java.util.Set;
 import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf;
 import org.checkerframework.checker.nonempty.qual.PolyNonEmpty;
 import org.checkerframework.dataflow.qual.Pure;
@@ -31,9 +33,19 @@ public boolean isEmpty() {
 
   @EnsuresNonEmptyIf(result = false, expression = "this")
   public boolean isEmpty2() {
+    // :: error: contracts.conditional.postcondition
     return size() == 0 ? true : false;
   }
 
+  Set<Object> set = new HashSet<>();
+
+  @EnsuresNonEmptyIf(result = false, expression = "this.set")
+  public boolean isEmpty2B() {
+    // TODO: this is a false positive
+    // :: error: contracts.conditional.postcondition
+    return set.size() == 0 ? true : false;
+  }
+
   @EnsuresNonEmptyIf(result = false, expression = "this")
   public boolean isEmpty3() {
     return size() == 0;

diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
@@ -772,7 +772,9 @@ public void clearValue(JavaExpression expr) {
     } else if (expr instanceof ClassName) {
       ClassName c = (ClassName) expr;
       classValues.remove(c);
-    } else { // thisValue ...
+    } else if (expr instanceof ThisReference) {
+      thisValue = null;
+    } else {
       // No other types of expressions are stored.
     }
   }
@@ -1190,9 +1192,10 @@ private S upperBound(S other, boolean shouldWiden) {
     {
       V otherVal = other.thisValue;
       V myVal = thisValue;
-      V mergedVal = myVal == null ? null : upperBoundOfValues(otherVal, myVal, shouldWiden);
-      if (mergedVal != null) {
-        newStore.thisValue = mergedVal;
+      if (myVal == null || otherVal == null) {
+        newStore.thisValue = null;
+      } else {
+        newStore.thisValue = upperBoundOfValues(otherVal, myVal, shouldWiden);
       }
     }