added tests

plugins/formal-verification/testData/diagnostics/good_contracts/stdlib_replacement_tests.kt

@@ -1,17 +1,33 @@
 // REPLACE_STDLIB_EXTENSIONS
+// ALWAYS_VALIDATE
 
-import kotlin.contracts.contract
-import kotlin.contracts.ExperimentalContracts
+import org.jetbrains.kotlin.formver.plugin.verify
 
-@OptIn(ExperimentalContracts::class)
-fun <!VIPER_TEXT!>useRepeat<!>(): Unit {
-    contract {
-        returns()
-    }
+fun <!VIPER_TEXT!>useChecks<!>(): Unit {
     check(true)
     check(true) { "Lazy message" }
 }
 
 // TODO: add test for `repeat` (we actually have a bug there because we require unsatisfied precondition in loops)
 
-// TODO: add tests for `let`, `apply`, `with`, `run`, `also`
+fun <!VIPER_TEXT!>useRuns<!>(x: Int): Unit {
+    verify(run { x + 1 } == 1 + x)
+    verify(x.run { plus(1) } == 1 + x)
+}
+
+fun <!VIPER_TEXT!>useAlso<!>(x: Int): Unit {
+    (x + 1).also { verify(it == 1 + x) }
+}
+
+fun <!VIPER_TEXT!>useLet<!>(x: Int): Unit {
+    verify(x.let { it + 1 } == 1 + x)
+}
+
+fun <!VIPER_TEXT!>useWith<!>(x: Int): Unit {
+    with(x + 1) { verify(this == 1 + x) }
+}
+
+fun <!VIPER_TEXT!>useApply<!>(x: Int): Unit {
+    (x + 1).apply { verify(this == 1 + x) }
+}
+

plugins/formal-verification/testData/stdlibReplacements.kt

@@ -1,5 +1,4 @@
 import org.jetbrains.kotlin.formver.plugin.NeverConvert
-import org.jetbrains.kotlin.formver.plugin.verify
 
 @NeverConvert
 inline fun <T> run(block: () -> T): T = block()
@@ -17,7 +16,7 @@ inline fun <T> T.also(block: (T) -> Unit): T {
 inline fun <T, R> T.let(block: (T) -> R): R = block(this)
 
 @NeverConvert
-inline fun <T> T.apply(block: T.() -> Unit): T = {
+inline fun <T> T.apply(block: T.() -> Unit): T {
     this.block()
     return this
 }