FIR checker: report errors in contract description
This commit is contained in:
committed by
TeamCityServer
parent
3d635b6a94
commit
20f9787c70
+4
-4
@@ -32,12 +32,12 @@ fun case_2() {
|
||||
class case_4 : ClassLevel3() {
|
||||
|
||||
fun <T : Number?>T.case_4_1(): Boolean {
|
||||
contract { returns(false) implies (<!UNRESOLVED_LABEL!>this@case_4<!> !is ClassLevel1) }
|
||||
contract { <!ERROR_IN_CONTRACT_DESCRIPTION!>returns(false) implies (<!UNRESOLVED_LABEL!>this@case_4<!> !is ClassLevel1)<!> }
|
||||
return this == null
|
||||
}
|
||||
|
||||
fun <T : Boolean>T.case_4_2() {
|
||||
contract { returns() implies (!this@case_4_2) }
|
||||
contract { <!ERROR_IN_CONTRACT_DESCRIPTION!>returns() implies (!this@case_4_2)<!> }
|
||||
if (this) throw Exception()
|
||||
}
|
||||
|
||||
@@ -60,12 +60,12 @@ class case_4 : ClassLevel3() {
|
||||
class case_5<T> : ClassLevel5() {
|
||||
inner class case_5_1 {
|
||||
fun <K : Number?>K.case_5_1_1() {
|
||||
contract { returns() implies (<!UNRESOLVED_LABEL!>this@case_5_1<!> !is ClassLevel1 && <!UNRESOLVED_LABEL!>this@case_5_1<!> != null || <!UNRESOLVED_LABEL!>this@case_5<!> is ClassLevel1 && this@case_5_1_1 is Float) }
|
||||
contract { <!ERROR_IN_CONTRACT_DESCRIPTION!>returns() implies (<!UNRESOLVED_LABEL!>this@case_5_1<!> !is ClassLevel1 && <!UNRESOLVED_LABEL!>this@case_5_1<!> != null || <!UNRESOLVED_LABEL!>this@case_5<!> is ClassLevel1 && this@case_5_1_1 is Float)<!> }
|
||||
if (!(this@case_5_1 !is ClassLevel1 && this@case_5_1 != null || this@case_5 is ClassLevel1 && this is Float)) throw Exception()
|
||||
}
|
||||
|
||||
fun case_5_1_2() {
|
||||
contract { returns() implies (<!UNRESOLVED_LABEL!>this@case_5_1<!> !is ClassLevel1 || <!UNRESOLVED_LABEL!>this@case_5<!> is ClassLevel1 || <!UNRESOLVED_LABEL!>this@case_5_1<!> == null) }
|
||||
contract { <!ERROR_IN_CONTRACT_DESCRIPTION!>returns() implies (<!UNRESOLVED_LABEL!>this@case_5_1<!> !is ClassLevel1 || <!UNRESOLVED_LABEL!>this@case_5<!> is ClassLevel1 || <!UNRESOLVED_LABEL!>this@case_5_1<!> == null)<!> }
|
||||
if (!(this@case_5_1 !is ClassLevel1 || this@case_5 is ClassLevel1 || this@case_5_1 == null)) throw Exception()
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user