File tree Expand file tree Collapse file tree 1 file changed +14
-5
lines changed
usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter Expand file tree Collapse file tree 1 file changed +14
-5
lines changed Original file line number Diff line number Diff line change @@ -985,16 +985,25 @@ class JcExprResolver(
985985 }
986986
987987 /* *
988- * Always use negative addresses in enum static initializers,
989- * for static initializers of other classes depends on [JcContext.useNegativeAddressesInStaticInitializer].
988+ * Always use negative addresses in enum static initializers and enum methods
989+ * that were reached from the corresponding static initializer, for static initializers of other classes
990+ * depends on [JcContext.useNegativeAddressesInStaticInitializer].
990991 */
991992 fun JcState.useStaticAddressForAllocation (): Boolean {
992- val isEnumStaticInitializer = lastEnteredMethod.let { it.isClassInitializer && it.enclosingClass.isEnum }
993- if (isEnumStaticInitializer) {
993+ val staticInitializers = callStack.filter { it.method.isClassInitializer }
994+
995+ // Enum's static initializer may contain invocations of other methods – from this enum or from other classes.
996+ // In case of enum methods, we need to consider all refs allocated in these methods as static too. It is important
997+ // because these refs may be assigned to enum's static fields – $VALUES, for example.
998+ val currentClass = lastEnteredMethod.enclosingClass
999+ val inEnumMethodFromEnumStaticInitializer =
1000+ currentClass.isEnum && staticInitializers.any { it.method.enclosingClass == currentClass }
1001+
1002+ if (inEnumMethodFromEnumStaticInitializer) {
9941003 return true
9951004 }
9961005
997- return ctx.useNegativeAddressesInStaticInitializer && callStack.any { it.method.isClassInitializer }
1006+ return ctx.useNegativeAddressesInStaticInitializer && staticInitializers.isNotEmpty()
9981007 }
9991008
10001009 /* *
You can’t perform that action at this time.
0 commit comments