update unique to top on assignment

jesyspa · Jul 25, 2024 · cc0cc24 · cc0cc24
1 parent 51b9c07
commit cc0cc24
Showing 1 changed file with 4 additions and 0 deletions.
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
@@ -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