Improve exception handling in CalledMethodsTransfer.accumulate (#6233)

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())));
     }
   }
 

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;
+    }
+  }
+}