added tests for check with empty implementation

plugins/formal-verification/testData/diagnostics/good_contracts/stdlib_replacement_tests.fir.diag.txt

@@ -0,0 +1,16 @@
+/stdlib_replacement_tests.kt:(151,160): info: Generated Viper text for useRepeat:
+method global$fun_useRepeat$fun_take$$return$T_Unit() returns (ret$0: Ref)
+  ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(ret$0), dom$RuntimeType$unitType())
+  ensures true
+{
+  var ret$1: Ref
+  var anonymous$0: Ref
+  var ret$2: Ref
+  var anonymous$1: Ref
+  ret$0 := dom$RuntimeType$unitValue()
+  anonymous$0 := dom$RuntimeType$boolToRef(true)
+  label label$ret$1
+  anonymous$1 := dom$RuntimeType$boolToRef(true)
+  label label$ret$2
+  label label$ret$0
+}

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

@@ -0,0 +1,17 @@
+// REPLACE_STDLIB_EXTENSIONS
+
+import kotlin.contracts.contract
+import kotlin.contracts.ExperimentalContracts
+
+@OptIn(ExperimentalContracts::class)
+fun <!VIPER_TEXT!>useRepeat<!>(): Unit {
+    contract {
+        returns()
+    }
+    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`

plugins/formal-verification/testData/stdlibReplacements.kt

@@ -1,4 +1,5 @@
 import org.jetbrains.kotlin.formver.plugin.NeverConvert
+import org.jetbrains.kotlin.formver.plugin.verify
 
 @NeverConvert
 inline fun <T> run(block: () -> T): T = block()
@@ -23,3 +24,23 @@ inline fun <T> T.apply(block: T.() -> Unit): T = {
 
 @NeverConvert
 inline fun <T, R> with(receiver: T, block: T.() -> R): R = receiver.block()
+
+@NeverConvert
+inline fun repeat(times: Int, action: (Int) -> Unit) {
+    var counter: Int = 0
+    while (counter < times) {
+        action(counter)
+        counter = counter + 1
+    }
+}
+
+// `check`s are intended for runtime, we have our own `verify` to check static properties
+@NeverConvert
+inline fun check(value: Boolean) {
+}
+
+@NeverConvert
+inline fun check(value: Boolean, lazyMessage: () -> Any) {
+}
+
+