Skip to content

Commit

Permalink
Removal of Unused Entities After #216 (#225)
Browse files Browse the repository at this point in the history
  • Loading branch information
GrigoriiSolnyshkin authored and Eric-Song-Nop committed Jul 30, 2024
1 parent 1effbea commit 9dec3bf
Show file tree
Hide file tree
Showing 3 changed files with 1 addition and 14 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -5,22 +5,18 @@

package org.jetbrains.kotlin.formver.embeddings

import org.jetbrains.kotlin.contracts.description.EventOccurrencesRange
import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol
import org.jetbrains.kotlin.fir.types.ConeKotlinType
import org.jetbrains.kotlin.formver.viper.ast.Info

sealed interface SourceRole {
data class ParamFunctionLeakageCheck(val functionRole: FirSymbolHolder) : SourceRole

data class ListElementAccessCheck(val accessType: AccessCheckType) : SourceRole {
enum class AccessCheckType {
LESS_THAN_ZERO,
GREATER_THAN_LIST_SIZE
}
}

data class CallsInPlaceEffect(val paramSymbol: FirBasedSymbol<*>, val kind: EventOccurrencesRange) : SourceRole
data class ConditionalEffect(val effect: ReturnsEffect, val condition: Condition) : SourceRole
data class FirSymbolHolder(val firSymbol: FirBasedSymbol<*>) : SourceRole, Condition

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,15 +5,9 @@

package org.jetbrains.kotlin.formver.embeddings.callables

import org.jetbrains.kotlin.formver.domains.FunctionBuilder
import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain
import org.jetbrains.kotlin.formver.viper.ast.*


object SpecialFunctions {
val duplicableFunction = FunctionBuilder.build("duplicable") {
argument { Type.Ref }
returns { Type.Bool }
}
val all = listOf(duplicableFunction) + RuntimeTypeDomain.accompanyingFunctions
val all = RuntimeTypeDomain.accompanyingFunctions
}
Original file line number Diff line number Diff line change
Expand Up @@ -218,9 +218,6 @@ function special$divInts(arg1: Ref, arg2: Ref): Ref
dom$RuntimeType$intFromRef(arg1) / dom$RuntimeType$intFromRef(arg2)


function special$duplicable(arg1: Ref): Bool


function special$geInts(arg1: Ref, arg2: Ref): Ref
ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(result), dom$RuntimeType$boolType())
ensures dom$RuntimeType$boolFromRef(result) ==
Expand Down

0 comments on commit 9dec3bf

Please sign in to comment.