Add spec tests for contracts
This commit is contained in:
+82
@@ -0,0 +1,82 @@
|
||||
// !LANGUAGE: +AllowContractsForCustomFunctions +UseReturnsEffect +UseCallsInPlaceEffect
|
||||
// !DIAGNOSTICS: -INVISIBLE_REFERENCE -INVISIBLE_MEMBER
|
||||
// !USE_EXPERIMENTAL: kotlin.contracts.ExperimentalContracts
|
||||
|
||||
/*
|
||||
KOTLIN DIAGNOSTICS NOT LINKED SPEC TEST (NEGATIVE)
|
||||
|
||||
SECTION: contracts
|
||||
CATEGORY: analysis, common
|
||||
NUMBER: 1
|
||||
DESCRIPTION: Analysis by contracts with mixed CallsInPlace and Returns effects.
|
||||
*/
|
||||
|
||||
// FILE: contracts.kt
|
||||
|
||||
package contracts
|
||||
|
||||
import kotlin.contracts.*
|
||||
|
||||
inline fun case_1(value_1: Int?, block: () -> Unit): Boolean {
|
||||
contract {
|
||||
callsInPlace(block, InvocationKind.AT_MOST_ONCE)
|
||||
returns(true) implies (value_1 != null)
|
||||
}
|
||||
|
||||
block()
|
||||
|
||||
return value_1 != null
|
||||
}
|
||||
|
||||
inline fun <T> T?.case_2(value_1: Int?, value_2: Any?, block: () -> Unit): Boolean? {
|
||||
contract {
|
||||
callsInPlace(block, InvocationKind.AT_MOST_ONCE)
|
||||
returns(true) implies (value_1 == null && this@case_2 == null && value_2 !is Boolean?)
|
||||
returns(false) implies (value_2 is Boolean?)
|
||||
returns(null) implies ((value_1 != null || this@case_2 != null) && value_2 !is Boolean?)
|
||||
}
|
||||
|
||||
block()
|
||||
|
||||
if (value_1 != null && this != null && value_2 is Boolean?) return true
|
||||
if (value_2 !is Boolean?) return false
|
||||
|
||||
return null
|
||||
}
|
||||
|
||||
// FILE: usages.kt
|
||||
|
||||
import contracts.*
|
||||
|
||||
fun case_1(value_1: Int?) {
|
||||
val value_2: Int
|
||||
if (contracts.case_1(value_1) { value_2 = 10 }) {
|
||||
println(<!UNINITIALIZED_VARIABLE!>value_2<!>)
|
||||
} else {
|
||||
value_1<!UNSAFE_CALL!>.<!>inv()
|
||||
println(value_2)
|
||||
}
|
||||
}
|
||||
|
||||
fun case_2(value_1: Int?, value_2: Int?, value_3: Any?) {
|
||||
val value_4: Int
|
||||
when (value_1.case_2(value_2, value_3) { value_4 = 10 }) {
|
||||
true -> {
|
||||
println(value_3?.<!UNRESOLVED_REFERENCE_WRONG_RECEIVER!>xor<!>(true))
|
||||
println(<!UNINITIALIZED_VARIABLE!>value_4<!>)
|
||||
println(<!DEBUG_INFO_CONSTANT!>value_1<!><!UNSAFE_CALL!>.<!>inv())
|
||||
println(<!DEBUG_INFO_CONSTANT!>value_2<!><!UNSAFE_CALL!>.<!>inv())
|
||||
}
|
||||
false -> {
|
||||
println(value_4)
|
||||
println(value_1)
|
||||
println(value_2)
|
||||
}
|
||||
null -> {
|
||||
println(value_3?.<!UNRESOLVED_REFERENCE_WRONG_RECEIVER!>xor<!>(true))
|
||||
println(value_4)
|
||||
println(value_1)
|
||||
println(value_2)
|
||||
}
|
||||
}
|
||||
}
|
||||
+17
@@ -0,0 +1,17 @@
|
||||
package
|
||||
|
||||
public fun case_1(/*0*/ value_1: kotlin.Int?): kotlin.Unit
|
||||
public fun case_2(/*0*/ value_1: kotlin.Int?, /*1*/ value_2: kotlin.Int?, /*2*/ value_3: kotlin.Any?): kotlin.Unit
|
||||
|
||||
package contracts {
|
||||
public inline fun case_1(/*0*/ value_1: kotlin.Int?, /*1*/ block: () -> kotlin.Unit): kotlin.Boolean
|
||||
CallsInPlace(block, AT_MOST_ONCE)
|
||||
Returns(TRUE) -> value_1 != null
|
||||
|
||||
public inline fun </*0*/ T> T?.case_2(/*0*/ value_1: kotlin.Int?, /*1*/ value_2: kotlin.Any?, /*2*/ block: () -> kotlin.Unit): kotlin.Boolean?
|
||||
CallsInPlace(block, AT_MOST_ONCE)
|
||||
Returns(TRUE) -> value_1 == null && <this> == null && value_2 !is Boolean?
|
||||
Returns(FALSE) -> value_2 is Boolean?
|
||||
Returns(NULL) -> (value_1 != null || <this> != null) && value_2 !is Boolean?
|
||||
|
||||
}
|
||||
+78
@@ -0,0 +1,78 @@
|
||||
// !LANGUAGE: +AllowContractsForCustomFunctions +UseReturnsEffect +UseCallsInPlaceEffect
|
||||
// !DIAGNOSTICS: -INVISIBLE_REFERENCE -INVISIBLE_MEMBER
|
||||
// !USE_EXPERIMENTAL: kotlin.contracts.ExperimentalContracts
|
||||
|
||||
/*
|
||||
KOTLIN DIAGNOSTICS NOT LINKED SPEC TEST (POSITIVE)
|
||||
|
||||
SECTION: contracts
|
||||
CATEGORY: analysis, common
|
||||
NUMBER: 1
|
||||
DESCRIPTION: Analysis by contracts with mixed CallsInPlace and Returns effects.
|
||||
*/
|
||||
|
||||
// FILE: contracts.kt
|
||||
|
||||
package contracts
|
||||
|
||||
import kotlin.contracts.*
|
||||
|
||||
inline fun case_1(value_1: Int?, block: () -> Unit): Boolean {
|
||||
contract {
|
||||
callsInPlace(block, InvocationKind.EXACTLY_ONCE)
|
||||
returns(true) implies (value_1 != null)
|
||||
}
|
||||
block()
|
||||
return value_1 != null
|
||||
}
|
||||
|
||||
inline fun <T> T?.case_2(value_1: Int?, value_2: Any?, block: () -> Unit): Boolean? {
|
||||
contract {
|
||||
callsInPlace(block, InvocationKind.EXACTLY_ONCE)
|
||||
returns(true) implies (value_1 != null && this@case_2 != null && value_2 is Boolean?)
|
||||
returns(false) implies (value_2 !is Boolean?)
|
||||
returns(null) implies ((value_1 == null || this@case_2 == null) && value_2 is Boolean?)
|
||||
}
|
||||
block()
|
||||
if (value_1 != null && this != null && value_2 is Boolean?) return true
|
||||
if (value_2 !is Boolean?) return false
|
||||
return null
|
||||
}
|
||||
|
||||
// FILE: usages.kt
|
||||
|
||||
import contracts.*
|
||||
|
||||
fun case_1(value_1: Int?) {
|
||||
val value_3: Int
|
||||
if (contracts.case_1(value_1) { value_3 = 10 }) {
|
||||
<!DEBUG_INFO_SMARTCAST!>value_1<!>.inv()
|
||||
println(value_3)
|
||||
} else {
|
||||
println(value_3)
|
||||
}
|
||||
}
|
||||
|
||||
fun case_2(value_1: Int?, value_2: Int?, value_3: Any?) {
|
||||
val value_4: Int
|
||||
when (value_1.case_2(value_2, value_3) { value_4 = 10 }) {
|
||||
true -> {
|
||||
println(<!DEBUG_INFO_SMARTCAST!>value_3<!>?.xor(true))
|
||||
println(value_4)
|
||||
println(<!DEBUG_INFO_SMARTCAST!>value_1<!>.inv())
|
||||
println(<!DEBUG_INFO_SMARTCAST!>value_2<!>.inv())
|
||||
}
|
||||
false -> {
|
||||
println(value_4)
|
||||
println(value_1)
|
||||
println(value_2)
|
||||
}
|
||||
null -> {
|
||||
println(<!DEBUG_INFO_SMARTCAST!>value_3<!>?.xor(true))
|
||||
println(value_4)
|
||||
println(value_1)
|
||||
println(value_2)
|
||||
}
|
||||
}
|
||||
println(value_4)
|
||||
}
|
||||
+17
@@ -0,0 +1,17 @@
|
||||
package
|
||||
|
||||
public fun case_1(/*0*/ value_1: kotlin.Int?): kotlin.Unit
|
||||
public fun case_2(/*0*/ value_1: kotlin.Int?, /*1*/ value_2: kotlin.Int?, /*2*/ value_3: kotlin.Any?): kotlin.Unit
|
||||
|
||||
package contracts {
|
||||
public inline fun case_1(/*0*/ value_1: kotlin.Int?, /*1*/ block: () -> kotlin.Unit): kotlin.Boolean
|
||||
CallsInPlace(block, EXACTLY_ONCE)
|
||||
Returns(TRUE) -> value_1 != null
|
||||
|
||||
public inline fun </*0*/ T> T?.case_2(/*0*/ value_1: kotlin.Int?, /*1*/ value_2: kotlin.Any?, /*2*/ block: () -> kotlin.Unit): kotlin.Boolean?
|
||||
CallsInPlace(block, EXACTLY_ONCE)
|
||||
Returns(TRUE) -> value_1 != null && <this> != null && value_2 is Boolean?
|
||||
Returns(FALSE) -> value_2 !is Boolean?
|
||||
Returns(NULL) -> (value_1 == null || <this> == null) && value_2 is Boolean?
|
||||
|
||||
}
|
||||
+35
@@ -0,0 +1,35 @@
|
||||
// !LANGUAGE: +AllowContractsForCustomFunctions +UseReturnsEffect
|
||||
// !USE_EXPERIMENTAL: kotlin.contracts.ExperimentalContracts
|
||||
// !WITH_CONTRACT_FUNCTIONS
|
||||
// SKIP_TXT
|
||||
|
||||
/*
|
||||
KOTLIN DIAGNOSTICS NOT LINKED SPEC TEST (POSITIVE)
|
||||
|
||||
SECTION: contracts
|
||||
CATEGORY: analysis, common
|
||||
NUMBER: 2
|
||||
DESCRIPTION: Recursion in the lambda of contract function.
|
||||
*/
|
||||
|
||||
fun case_1(x: Int): Unit = funWithExactlyOnceCallsInPlace {
|
||||
if (x == 0) return
|
||||
if (x == 1) return
|
||||
return case_1(x - 2)
|
||||
}
|
||||
|
||||
fun case_2(x: Int) {
|
||||
funWithAtLeastOnceCallsInPlace {
|
||||
if (x == 0) return
|
||||
if (x == 1) return
|
||||
return case_2(x - 2)
|
||||
}
|
||||
}
|
||||
|
||||
fun case_3(x: Int) {
|
||||
funWithAtMostOnceCallsInPlace {
|
||||
if (x == 0) return
|
||||
if (x == 1) return
|
||||
return case_3(x - 2)
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user