From 05863eb52129841b79279b4995663a21a4a5eb01 Mon Sep 17 00:00:00 2001
From: Calvin Loncaric <marvinx03@gmail.com>
Date: Tue, 10 Oct 2023 05:43:41 -0700
Subject: [PATCH] Improve exception handling in
 `CalledMethodsTransfer.accumulate` (#6233)

---
 .../calledmethods/CalledMethodsTransfer.java  |  5 ++-
 .../tests/calledmethods/ExceptionalPath2.java | 37 +++++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 checker/tests/calledmethods/ExceptionalPath2.java

diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java
index 72b70198b52..bf05616fe8a 100644
--- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java
+++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java
@@ -115,7 +115,10 @@ public void accumulate(
         }
       }
       AnnotationMirror newAnno = atypeFactory.createAccumulatorAnnotation(valuesAsList);
-      exceptionalStores.forEach((tm, s) -> s.insertValue(target, newAnno));
+      exceptionalStores.forEach(
+          (tm, s) ->
+              s.replaceValue(
+                  target, analysis.createSingleAnnotationValue(newAnno, target.getType())));
     }
   }
 
diff --git a/checker/tests/calledmethods/ExceptionalPath2.java b/checker/tests/calledmethods/ExceptionalPath2.java
new file mode 100644
index 00000000000..795de45185a
--- /dev/null
+++ b/checker/tests/calledmethods/ExceptionalPath2.java
@@ -0,0 +1,37 @@
+import java.io.IOException;
+import org.checkerframework.checker.calledmethods.qual.*;
+
+class ExceptionalPath2 {
+
+  interface Resource {
+    void a();
+
+    void b() throws IOException;
+  }
+
+  Resource r;
+
+  // Regression test for an obscure bug: in some cases, the called
+  // methods transfer function would silently fail to update the
+  // set of known called methods along exceptional paths.  That
+  // would a spurious precondition error on this method.
+  @EnsuresCalledMethods(
+      value = "this.r",
+      methods = {"b"})
+  void test() {
+    try {
+      try {
+        r.a();
+      } finally {
+        r.b();
+      }
+    } catch (IOException ignored) {
+      // The only way to get here is if `r.b()` started running and
+      // threw an IOException.  We no longer know whether `r.a()`
+      // has been called, since `r.b()` might have overwritten `r`
+      // before throwing.
+      // ::error: (assignment)
+      @CalledMethods({"a"}) Resource x = r;
+    }
+  }
+}