Skip to content

Commit 558e0d9

Browse files
committed
Rebase fixes
1 parent ca99356 commit 558e0d9

File tree

4 files changed

+12
-28
lines changed

4 files changed

+12
-28
lines changed

usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,15 @@
11
package org.usvm.api.checkers
22

3-
import org.jacodb.ets.base.EtsIfStmt
4-
import org.jacodb.ets.base.EtsStmt
3+
import org.jacodb.ets.model.EtsIfStmt
54
import org.jacodb.ets.model.EtsMethod
5+
import org.jacodb.ets.model.EtsStmt
66
import org.usvm.machine.TsInterpreterObserver
77
import org.usvm.machine.expr.TsSimpleValueResolver
88
import org.usvm.machine.interpreter.TsStepScope
99
import org.usvm.machine.state.TsState
1010
import org.usvm.statistics.UMachineObserver
11+
import kotlin.collections.filter
12+
import kotlin.collections.isNotEmpty
1113

1214
data class UncoveredIfSuccessors(val ifStmt: EtsIfStmt, val successors: Set<EtsStmt>)
1315

usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt

Lines changed: 5 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,10 @@
11
package org.usvm.machine
22

3-
import org.jacodb.ets.base.EtsAssignStmt
4-
import org.jacodb.ets.base.EtsCallExpr
5-
import org.jacodb.ets.base.EtsGotoStmt
6-
import org.jacodb.ets.base.EtsIfStmt
7-
import org.jacodb.ets.base.EtsReturnStmt
8-
import org.jacodb.ets.base.EtsSwitchStmt
9-
import org.jacodb.ets.base.EtsThrowStmt
3+
import org.jacodb.ets.model.EtsAssignStmt
4+
import org.jacodb.ets.model.EtsCallExpr
5+
import org.jacodb.ets.model.EtsIfStmt
6+
import org.jacodb.ets.model.EtsReturnStmt
7+
import org.jacodb.ets.model.EtsThrowStmt
108
import org.usvm.UBoolExpr
119
import org.usvm.machine.expr.TsSimpleValueResolver
1210
import org.usvm.machine.interpreter.TsStepScope
@@ -66,20 +64,4 @@ interface TsInterpreterObserver : UInterpreterObserver {
6664
) {
6765
// default empty implementation
6866
}
69-
70-
fun onGotoStatement(
71-
simpleValueResolver: TsSimpleValueResolver,
72-
stmt: EtsGotoStmt,
73-
scope: TsStepScope,
74-
) {
75-
// default empty implementation
76-
}
77-
78-
fun onSwitchStatement(
79-
simpleValueResolver: TsSimpleValueResolver,
80-
stmt: EtsSwitchStmt,
81-
scope: TsStepScope,
82-
) {
83-
// default empty implementation
84-
}
8567
}

usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
package org.usvm.samples.checkers
22

3-
import org.jacodb.ets.base.EtsAssignStmt
4-
import org.jacodb.ets.base.EtsIfStmt
3+
import org.jacodb.ets.model.EtsAssignStmt
4+
import org.jacodb.ets.model.EtsIfStmt
55
import org.jacodb.ets.model.EtsScene
66
import org.jacodb.ets.utils.loadEtsFileAutoConvert
77
import org.junit.jupiter.api.Test

usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,4 +23,4 @@ class UnreachableCode {
2323

2424
return
2525
}
26-
}
26+
}

0 commit comments

Comments
 (0)