Rename InvocationKind to EventOccurrencesRange
This commit is contained in:
@@ -53,7 +53,7 @@ class ReturnsEffectDeclaration(val value: ConstantReference) : EffectDeclaration
|
||||
* Effect which specifies, that during execution of subroutine, callable [variableReference] will be invoked
|
||||
* [kind] amount of times, and will never be invoked after subroutine call is finished.
|
||||
*/
|
||||
class CallsEffectDeclaration(val variableReference: VariableReference, val kind: InvocationKind) : EffectDeclaration {
|
||||
class CallsEffectDeclaration(val variableReference: VariableReference, val kind: EventOccurrencesRange) : EffectDeclaration {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitCallsEffectDeclaration(this, data)
|
||||
}
|
||||
+38
@@ -0,0 +1,38 @@
|
||||
/*
|
||||
* Copyright 2010-2018 JetBrains s.r.o. and Kotlin Programming Language contributors.
|
||||
* Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file.
|
||||
*/
|
||||
|
||||
package org.jetbrains.kotlin.contracts.description
|
||||
|
||||
import kotlin.math.max
|
||||
import kotlin.math.min
|
||||
|
||||
enum class EventOccurrencesRange(private val left: Int, private val right: Int) {
|
||||
ZERO(0, 0), // 0..0
|
||||
AT_MOST_ONCE(0, 1), // 0..1
|
||||
EXACTLY_ONCE(1, 1), // 1..1
|
||||
AT_LEAST_ONCE(1, 2), // 1..*
|
||||
UNKNOWN(0, 2); // 0..*
|
||||
|
||||
companion object {
|
||||
private fun fromRange(left: Int, right: Int): EventOccurrencesRange = when (min(left, 1) to min(right, 2)) {
|
||||
0 to 0 -> ZERO
|
||||
0 to 1 -> AT_MOST_ONCE
|
||||
1 to 1 -> EXACTLY_ONCE
|
||||
1 to 2 -> AT_LEAST_ONCE
|
||||
0 to 2 -> UNKNOWN
|
||||
else -> throw IllegalArgumentException()
|
||||
}
|
||||
|
||||
fun or(x: EventOccurrencesRange, y: EventOccurrencesRange): EventOccurrencesRange = fromRange(min(x.left, y.left), max(x.right, y.right))
|
||||
|
||||
fun plus(x: EventOccurrencesRange, y: EventOccurrencesRange): EventOccurrencesRange = fromRange(x.left + y.left, x.right + y.right)
|
||||
}
|
||||
|
||||
infix fun or(other: EventOccurrencesRange): EventOccurrencesRange = Companion.or(this, other)
|
||||
operator fun plus(other: EventOccurrencesRange): EventOccurrencesRange = Companion.plus(this, other)
|
||||
}
|
||||
|
||||
fun EventOccurrencesRange.isDefinitelyVisited(): Boolean = this == EventOccurrencesRange.EXACTLY_ONCE || this == EventOccurrencesRange.AT_LEAST_ONCE
|
||||
fun EventOccurrencesRange.canBeRevisited(): Boolean = this == EventOccurrencesRange.UNKNOWN || this == EventOccurrencesRange.AT_LEAST_ONCE
|
||||
@@ -1,38 +0,0 @@
|
||||
/*
|
||||
* Copyright 2010-2018 JetBrains s.r.o. and Kotlin Programming Language contributors.
|
||||
* Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file.
|
||||
*/
|
||||
|
||||
package org.jetbrains.kotlin.contracts.description
|
||||
|
||||
import kotlin.math.max
|
||||
import kotlin.math.min
|
||||
|
||||
enum class InvocationKind(private val left: Int, private val right: Int) {
|
||||
ZERO(0, 0), // 0..0
|
||||
AT_MOST_ONCE(0, 1), // 0..1
|
||||
EXACTLY_ONCE(1, 1), // 1..1
|
||||
AT_LEAST_ONCE(1, 2), // 1..*
|
||||
UNKNOWN(0, 2); // 0..*
|
||||
|
||||
companion object {
|
||||
private fun fromRange(left: Int, right: Int): InvocationKind = when (min(left, 1) to min(right, 2)) {
|
||||
0 to 0 -> ZERO
|
||||
0 to 1 -> AT_MOST_ONCE
|
||||
1 to 1 -> EXACTLY_ONCE
|
||||
1 to 2 -> AT_LEAST_ONCE
|
||||
0 to 2 -> UNKNOWN
|
||||
else -> throw IllegalArgumentException()
|
||||
}
|
||||
|
||||
fun or(x: InvocationKind, y: InvocationKind): InvocationKind = fromRange(min(x.left, y.left), max(x.right, y.right))
|
||||
|
||||
fun and(x: InvocationKind, y: InvocationKind): InvocationKind = fromRange(x.left + y.left, x.right + y.right)
|
||||
}
|
||||
|
||||
infix fun or(other: InvocationKind): InvocationKind = Companion.or(this, other)
|
||||
infix fun and(other: InvocationKind): InvocationKind = Companion.and(this, other)
|
||||
}
|
||||
|
||||
fun InvocationKind.isDefinitelyVisited(): Boolean = this == InvocationKind.EXACTLY_ONCE || this == InvocationKind.AT_LEAST_ONCE
|
||||
fun InvocationKind.canBeRevisited(): Boolean = this == InvocationKind.UNKNOWN || this == InvocationKind.AT_LEAST_ONCE
|
||||
@@ -16,12 +16,12 @@
|
||||
|
||||
package org.jetbrains.kotlin.contracts.model.structure
|
||||
|
||||
import org.jetbrains.kotlin.contracts.description.InvocationKind
|
||||
import org.jetbrains.kotlin.contracts.description.EventOccurrencesRange
|
||||
import org.jetbrains.kotlin.contracts.model.ESEffect
|
||||
import org.jetbrains.kotlin.contracts.model.ESValue
|
||||
import org.jetbrains.kotlin.contracts.model.SimpleEffect
|
||||
|
||||
data class ESCalls(val callable: ESValue, val kind: InvocationKind) : SimpleEffect() {
|
||||
data class ESCalls(val callable: ESValue, val kind: EventOccurrencesRange) : SimpleEffect() {
|
||||
override fun isImplies(other: ESEffect): Boolean? {
|
||||
if (other !is ESCalls) return null
|
||||
|
||||
|
||||
Reference in New Issue
Block a user