new test

plugins/formal-verification/testData/diagnostics/verifies/inlining/scoped_receivers.fir.diag.txt

@@ -0,0 +1,192 @@
+/scoped_receivers.kt:(407,433): info: Generated Viper text for with_run_extension_labeled:
+field bf$size: Ref
+
+method f$with_run_extension_labeled$TF$NT$Int(this$extension: Ref)
+  returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+{
+  var anon$13: Ref
+  var anon$14: Ref
+  var ret$1: Ref
+  var anon$15: Ref
+  var anon$16: Ref
+  var ret$3: Ref
+  var anon$0: Ref
+  var anon$17: Ref
+  var ret$4: Ref
+  var anon$1: Ref
+  var anon$18: Ref
+  var anon$19: Ref
+  var ret$5: Ref
+  var anon$2: Ref
+  var anon$20: Ref
+  var ret$6: Ref
+  var anon$3: Ref
+  var anon$21: Ref
+  var ret$7: Ref
+  var anon$4: Ref
+  var anon$22: Ref
+  var ret$8: Ref
+  var anon$5: Ref
+  var anon$23: Ref
+  var ret$9: Ref
+  var anon$6: Ref
+  var anon$24: Ref
+  var anon$25: Ref
+  var ret$10: Ref
+  var anon$7: Ref
+  var anon$26: Ref
+  var ret$11: Ref
+  var anon$8: Ref
+  var anon$27: Ref
+  var anon$28: Ref
+  var ret$12: Ref
+  var anon$29: Ref
+  var anon$30: Ref
+  var ret$14: Ref
+  var anon$9: Ref
+  var anon$31: Ref
+  var ret$15: Ref
+  var anon$10: Ref
+  var anon$32: Ref
+  var anon$33: Ref
+  var ret$16: Ref
+  var anon$11: Ref
+  var anon$34: Ref
+  var ret$17: Ref
+  var anon$12: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$nullable(df$rt$intType()))
+  ret$1 := df$rt$boolToRef(this$extension == df$rt$nullValue())
+  goto lbl$ret$1
+  label lbl$ret$1
+  anon$14 := ret$1
+  if (df$rt$boolFromRef(anon$14)) {
+    anon$13 := df$rt$boolToRef(true)
+  } else {
+    var ret$2: Ref
+    ret$2 := sp$notBool(df$rt$boolToRef(this$extension == df$rt$nullValue()))
+    goto lbl$ret$2
+    label lbl$ret$2
+    anon$13 := ret$2
+  }
+  assert df$rt$boolFromRef(anon$13)
+  anon$0 := df$rt$boolToRef(true)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$boolType())
+  anon$1 := anon$0
+  anon$2 := df$rt$nullValue()
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$2), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$2), df$rt$nullable(df$rt$nothingType()))
+  anon$3 := anon$2
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$nullable(df$rt$intType()))
+  anon$4 := anon$3
+  ret$7 := df$rt$boolToRef(anon$4 == df$rt$nullValue())
+  goto lbl$ret$7
+  label lbl$ret$7
+  anon$21 := ret$7
+  assert df$rt$boolFromRef(anon$21)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$nullable(df$rt$intType()))
+  anon$5 := anon$3
+  ret$8 := df$rt$boolToRef(anon$5 == df$rt$nullValue())
+  goto lbl$ret$8
+  label lbl$ret$8
+  anon$22 := ret$8
+  assert df$rt$boolFromRef(anon$22)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$nullable(df$rt$intType()))
+  anon$6 := anon$3
+  ret$9 := df$rt$boolToRef(anon$6 == df$rt$nullValue())
+  goto lbl$ret$9
+  label lbl$ret$9
+  anon$23 := ret$9
+  assert df$rt$boolFromRef(anon$23)
+  label lbl$ret$6
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$6), df$rt$unitType())
+  anon$20 := ret$6
+  ret$5 := anon$20
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$5), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$5
+  label lbl$ret$5
+  anon$19 := ret$5
+  anon$18 := anon$19
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$18), df$rt$unitType())
+  assert df$rt$boolFromRef(anon$1)
+  assert df$rt$boolFromRef(anon$1)
+  anon$7 := df$rt$boolToRef(false)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$7), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$7), df$rt$boolType())
+  anon$8 := anon$7
+  assert !df$rt$boolFromRef(anon$8)
+  assert !df$rt$boolFromRef(anon$8)
+  assert df$rt$boolFromRef(anon$1)
+  ret$12 := df$rt$boolToRef(this$extension == df$rt$nullValue())
+  goto lbl$ret$12
+  label lbl$ret$12
+  anon$28 := ret$12
+  if (df$rt$boolFromRef(anon$28)) {
+    anon$27 := df$rt$boolToRef(true)
+  } else {
+    var ret$13: Ref
+    ret$13 := sp$notBool(df$rt$boolToRef(this$extension ==
+      df$rt$nullValue()))
+    goto lbl$ret$13
+    label lbl$ret$13
+    anon$27 := ret$13
+  }
+  assert df$rt$boolFromRef(anon$27)
+  anon$9 := df$rt$boolToRef(false)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$9), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$9), df$rt$boolType())
+  anon$10 := anon$9
+  assert !df$rt$boolFromRef(anon$10)
+  assert !df$rt$boolFromRef(anon$10)
+  assert !df$rt$boolFromRef(anon$8)
+  anon$11 := df$rt$boolToRef(true)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$11), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$11), df$rt$boolType())
+  anon$12 := anon$11
+  assert !df$rt$boolFromRef(anon$10)
+  assert df$rt$boolFromRef(anon$12)
+  assert df$rt$boolFromRef(anon$12)
+  label lbl$ret$17
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$17), df$rt$unitType())
+  anon$34 := ret$17
+  ret$16 := anon$34
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$16), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$16
+  label lbl$ret$16
+  anon$33 := ret$16
+  anon$32 := anon$33
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$32), df$rt$unitType())
+  label lbl$ret$15
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$15), df$rt$unitType())
+  anon$31 := ret$15
+  ret$14 := anon$31
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$14), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$14
+  label lbl$ret$14
+  anon$30 := ret$14
+  anon$29 := anon$30
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$29), df$rt$unitType())
+  label lbl$ret$11
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$11), df$rt$unitType())
+  anon$26 := ret$11
+  ret$10 := anon$26
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$10), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$10
+  label lbl$ret$10
+  anon$25 := ret$10
+  anon$24 := anon$25
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$24), df$rt$unitType())
+  label lbl$ret$4
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$4), df$rt$unitType())
+  anon$17 := ret$4
+  ret$3 := anon$17
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$3), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$3
+  label lbl$ret$3
+  anon$16 := ret$3
+  anon$15 := anon$16
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$15), df$rt$unitType())
+  label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+}

plugins/formal-verification/testData/diagnostics/verifies/inlining/scoped_receivers.kt

@@ -0,0 +1,51 @@
+// REPLACE_STDLIB_EXTENSIONS
+
+import org.jetbrains.kotlin.formver.plugin.NeverConvert
+import org.jetbrains.kotlin.formver.plugin.AlwaysVerify
+import org.jetbrains.kotlin.formver.plugin.verify
+
+@Suppress("NOTHING_TO_INLINE")
+@NeverConvert
+inline fun Int?.isNull() = this == null
+
+@Suppress("NOTHING_TO_INLINE")
+@NeverConvert
+inline fun Int?.isNotNull() = this != null
+
+@Suppress("LABEL_NAME_CLASH")
+fun Int?.<!VIPER_TEXT!>with_run_extension_labeled<!>() {
+    verify(isNull() || this@with_run_extension_labeled.isNotNull())
+    with(true) {
+        with(null) {
+            verify(
+                isNull(),
+                this.isNull(),
+                this@with.isNull(),
+            )
+        }
+        verify(this, this@with)
+        false.run {
+            verify(
+                !this,
+                !this@run,
+                this@with,
+                this@with_run_extension_labeled.isNull() || isNotNull(),
+            )
+            with(false) {
+                verify(
+                    !this,
+                    !this@with,
+                    !this@run,
+                )
+                with(true) labeled_with@{
+                    verify(
+                        !this@with,
+                        this,
+                        this@labeled_with,
+                    )
+                }
+            }
+        }
+    }
+}
+