From cc0cc248191ea60dbab1ec6d1729c591e3370118 Mon Sep 17 00:00:00 2001
From: Yifan Song <Eric_YF_Song@outlook.com>
Date: Thu, 25 Jul 2024 19:59:03 +0200
Subject: [PATCH] update unique to top on assignment

---
 .../src/org/jetbrains/kotlin/formver/UniqueCFA.kt             | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt
index a171ee39128170..ec8a2b9131fc13 100644
--- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt
+++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt
@@ -14,6 +14,7 @@ import org.jetbrains.kotlin.fir.analysis.checkers.cfa.FirControlFlowChecker
 import org.jetbrains.kotlin.fir.analysis.checkers.context.CheckerContext
 import org.jetbrains.kotlin.fir.declarations.FirVariable
 import org.jetbrains.kotlin.fir.declarations.hasAnnotation
+import org.jetbrains.kotlin.fir.expressions.FirVariableAssignment
 import org.jetbrains.kotlin.fir.expressions.toResolvedCallableSymbol
 import org.jetbrains.kotlin.fir.references.FirResolvedNamedReference
 import org.jetbrains.kotlin.fir.references.symbol
@@ -135,6 +136,9 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker(
                 } else {
                     this.data.nodeUniqueLevel[usePos]?.set(node, rhsUniqueLevel)
                 }
+                if (usePos is VariableAssignmentNode || usePos is VariableDeclarationNode) {
+                    return dataForNode.transformValues { it.put(callee, setOf(UniqueLevel.Top)) }
+                }
                 return dataForNode
             }
             return dataForNode