Merge nullability tests into existing nullability.kt

Move tests from nullability_operations.kt into the existing
verification/nullability.kt file. Use file-level ALWAYS_VALIDATE
instead of per-function @AlwaysVerify to match the existing convention.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: jesyspa

formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java

@@ -494,12 +494,6 @@ public void testNullability() {
       runTest("formver.compiler-plugin/testData/diagnostics/verification/nullability.kt");
     }
 
-    @Test
-    @TestMetadata("nullability_operations.kt")
-    public void testNullability_operations() {
-      runTest("formver.compiler-plugin/testData/diagnostics/verification/nullability_operations.kt");
-    }
-
     @Test
     @TestMetadata("stdlib_replacement_tests.kt")
     public void testStdlib_replacement_tests() {

formver.compiler-plugin/testData/diagnostics/verification/nullability.fir.diag.txt

@@ -1,8 +1,98 @@
-/nullability.kt:(24,35): info: Generated Viper text for return_null:
+/nullability.kt:(83,94): info: Generated Viper text for return_null:
 method f$return_null$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
 {
   ret$0 := df$rt$nullValue()
   goto lbl$ret$0
   label lbl$ret$0
 }
+
+/nullability.kt:(115,133): info: Generated Viper text for elvisDefaultOnNull:
+method f$elvisDefaultOnNull$TF$() returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+  ensures df$rt$intFromRef(ret$0) == 42
+{
+  var l0$x: Ref
+  l0$x := df$rt$nullValue()
+  if (l0$x != df$rt$nullValue()) {
+    ret$0 := l0$x
+  } else {
+    ret$0 := df$rt$intToRef(42)}
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability.kt:(241,260): info: Generated Viper text for nullablePassthrough:
+method f$nullablePassthrough$TF$NT$Int(p$x: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
+  ensures ret$0 == p$x
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$intType()))
+  ret$0 := p$x
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability.kt:(347,364): info: Generated Viper text for returnNullLiteral:
+method f$returnNullLiteral$TF$() returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
+  ensures ret$0 == df$rt$nullValue()
+{
+  ret$0 := df$rt$nullValue()
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability.kt:(450,475): info: Generated Viper text for nullComparisonReturnsTrue:
+method f$nullComparisonReturnsTrue$TF$() returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
+  ensures df$rt$boolFromRef(ret$0) == true
+{
+  var l0$x: Ref
+  l0$x := df$rt$nullValue()
+  ret$0 := df$rt$boolToRef(l0$x == df$rt$nullValue())
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability.kt:(595,624): info: Generated Viper text for nonNullComparisonReturnsFalse:
+method f$nonNullComparisonReturnsFalse$TF$() returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
+  ensures df$rt$boolFromRef(ret$0) == false
+{
+  var l0$x: Ref
+  l0$x := df$rt$nullValue()
+  ret$0 := sp$notBool(df$rt$boolToRef(l0$x == df$rt$nullValue()))
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability.kt:(745,761): info: Generated Viper text for elvisWithNonNull:
+method f$elvisWithNonNull$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+  ensures df$rt$intFromRef(ret$0) == df$rt$intFromRef(p$x)
+{
+  var l0$y: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
+  l0$y := p$x
+  if (l0$y != df$rt$nullValue()) {
+    ret$0 := l0$y
+  } else {
+    ret$0 := df$rt$intToRef(0)}
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability.kt:(870,887): info: Generated Viper text for smartcastInBranch:
+method f$smartcastInBranch$TF$NT$Int(p$n: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$n), df$rt$nullable(df$rt$intType()))
+  if (!(p$n == df$rt$nullValue())) {
+    ret$0 := p$n
+    goto lbl$ret$0
+  }
+  ret$0 := df$rt$intToRef(0)
+  goto lbl$ret$0
+  label lbl$ret$0
+}

formver.compiler-plugin/testData/diagnostics/verification/nullability.kt

@@ -1,3 +1,58 @@
 // ALWAYS_VALIDATE
 
+import org.jetbrains.kotlin.formver.plugin.postconditions
+
 fun <!VIPER_TEXT!>return_null<!>(): Int? = null
+
+fun <!VIPER_TEXT!>elvisDefaultOnNull<!>(): Int {
+    postconditions<Int> {
+        it == 42
+    }
+    val x: Int? = null
+    return x ?: 42
+}
+
+fun <!VIPER_TEXT!>nullablePassthrough<!>(x: Int?): Int? {
+    postconditions<Int?> {
+        it == x
+    }
+    return x
+}
+
+fun <!VIPER_TEXT!>returnNullLiteral<!>(): Int? {
+    postconditions<Int?> {
+        it == null
+    }
+    return null
+}
+
+fun <!VIPER_TEXT!>nullComparisonReturnsTrue<!>(): Boolean {
+    postconditions<Boolean> {
+        it == true
+    }
+    val x: Int? = null
+    return x == null
+}
+
+fun <!VIPER_TEXT!>nonNullComparisonReturnsFalse<!>(): Boolean {
+    postconditions<Boolean> {
+        it == false
+    }
+    val x: Int? = null
+    return x != null
+}
+
+fun <!VIPER_TEXT!>elvisWithNonNull<!>(x: Int): Int {
+    postconditions<Int> {
+        it == x
+    }
+    val y: Int? = x
+    return y ?: 0
+}
+
+fun <!VIPER_TEXT!>smartcastInBranch<!>(n: Int?): Int {
+    if (n != null) {
+        return n
+    }
+    return 0
+}