From 9d5e920a738d981d32339286e2397f5d71a4a276 Mon Sep 17 00:00:00 2001
From: Michael Ernst <mernst@cs.washington.edu>
Date: Fri, 16 Jul 2021 13:04:34 -0700
Subject: [PATCH] Fix equality test; fixes #4806

Co-authored-by: Martin Kellogg <kelloggm@cs.washington.edu>
---
 .../EnsuresCalledMethodsThisLub.java          | 43 +++++++++++++++++++
 .../framework/flow/CFAbstractStore.java       |  4 ++
 2 files changed, 47 insertions(+)
 create mode 100644 checker/tests/calledmethods/EnsuresCalledMethodsThisLub.java

diff --git a/checker/tests/calledmethods/EnsuresCalledMethodsThisLub.java b/checker/tests/calledmethods/EnsuresCalledMethodsThisLub.java
new file mode 100644
index 00000000000..f666f946acd
--- /dev/null
+++ b/checker/tests/calledmethods/EnsuresCalledMethodsThisLub.java
@@ -0,0 +1,43 @@
+import org.checkerframework.checker.calledmethods.qual.CalledMethods;
+import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
+
+class EnsuresCalledMethodsThisLub {
+
+  @EnsuresCalledMethods(
+      value = "#1",
+      methods = {"toString", "equals"})
+  void call1(Object obj) {
+    obj.toString();
+    obj.equals(null);
+  }
+
+  @EnsuresCalledMethods(
+      value = "#1",
+      methods = {"toString", "hashCode"})
+  void call2(Object obj) {
+    obj.toString();
+    obj.hashCode();
+  }
+
+  void test(boolean b) {
+    if (b) {
+      call1(this);
+    } else {
+      call2(this);
+    }
+    @CalledMethods("toString") Object obj1 = this;
+    // :: error: (assignment)
+    @CalledMethods({"toString", "equals"}) Object obj2 = this;
+  }
+
+  void test_arg(Object arg, boolean b) {
+    if (b) {
+      call1(arg);
+    } else {
+      call2(arg);
+    }
+    @CalledMethods("toString") Object obj1 = arg;
+    // :: error: (assignment)
+    @CalledMethods({"toString", "equals"}) Object obj2 = arg;
+  }
+}
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 0c607c08dc1..f87f18f8112 100644
--- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
+++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
@@ -4,6 +4,7 @@
 import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 import java.util.StringJoiner;
 import java.util.concurrent.atomic.AtomicLong;
 import java.util.function.BinaryOperator;
@@ -1182,6 +1183,9 @@ protected boolean supersetOf(CFAbstractStore<V, S> other) {
         return false;
       }
     }
+    if (!Objects.equals(thisValue, other.thisValue)) {
+      return false;
+    }
     for (Map.Entry<FieldAccess, V> e : other.fieldValues.entrySet()) {
       FieldAccess key = e.getKey();
       V value = fieldValues.get(key);