@@ -12,6 +12,7 @@ import org.usvm.api.allocateStaticRef
12
12
import org.usvm.api.evalTypeEquals
13
13
import org.usvm.api.targets.JcTarget
14
14
import org.usvm.api.typeStreamOf
15
+ import org.usvm.forkblacklists.UForkBlackList
15
16
import org.usvm.jvm.JcApplicationBlockGraph
16
17
import org.usvm.machine.*
17
18
import org.usvm.machine.interpreter.JcExprResolver
@@ -31,6 +32,7 @@ import org.usvm.util.write
31
32
class JcBlockInterpreter (
32
33
private val ctx : JcContext ,
33
34
private val applicationGraph : JcApplicationBlockGraph ,
35
+ var forkBlackList : UForkBlackList <JcState , JcInst > = UForkBlackList .createDefault(),
34
36
) : UInterpreter<JcState>() {
35
37
36
38
companion object {
@@ -67,7 +69,7 @@ class JcBlockInterpreter(
67
69
}
68
70
}
69
71
70
- val solver = ctx.solver<JcType , JcContext >()
72
+ val solver = ctx.solver<JcType >()
71
73
72
74
val model = (solver.checkWithSoftConstraints(state.pathConstraints) as USatResult ).model
73
75
state.models = listOf (model)
@@ -82,7 +84,7 @@ class JcBlockInterpreter(
82
84
83
85
logger.debug(" Step: {}" , stmt)
84
86
85
- val scope = StepScope (state)
87
+ val scope = StepScope (state, forkBlackList )
86
88
87
89
// handle exception firstly
88
90
val result = state.methodResult
0 commit comments