From ba3ccd40ff3ed0ddb8e830b4032d9c13b079aac6 Mon Sep 17 00:00:00 2001
From: Suzanne Millstein <smillst@cs.washington.edu>
Date: Wed, 4 Dec 2024 11:54:41 -0800
Subject: [PATCH] False positive.

---
 checker/tests/nonempty/SizeInIsEmpty.java            | 12 ++++++++++++
 .../framework/flow/CFAbstractStore.java              | 11 +++++++----
 2 files changed, 19 insertions(+), 4 deletions(-)

diff --git a/checker/tests/nonempty/SizeInIsEmpty.java b/checker/tests/nonempty/SizeInIsEmpty.java
index 5b9ea07ae3c..31ca40ea5d2 100644
--- 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
index 93f96d70c87..8f31f26841b 100644
--- 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);
       }
     }