diff --git a/usvm-jvm/build.gradle.kts b/usvm-jvm/build.gradle.kts index daad5aa69b..0cf77dc8ac 100644 --- a/usvm-jvm/build.gradle.kts +++ b/usvm-jvm/build.gradle.kts @@ -24,7 +24,7 @@ val `usvm-api` by sourceSets.creating { val approximations by configurations.creating val approximationsRepo = "com.github.UnitTestBot.java-stdlib-approximations" -val approximationsVersion = "0f081f101e" +val approximationsVersion = "5f137507d6" dependencies { implementation(project(":usvm-core")) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt index cc42ff352b..128dfefae1 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt @@ -307,6 +307,16 @@ class JcInterpreter( return } + if (method.isFinal) { + // Case for approximated interfaces + with (stmt) { + scope.doWithState { + newStmt(JcConcreteMethodCallInst(location, method, arguments, returnSite)) + } + } + return + } + resolveVirtualInvoke(stmt, scope) } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt index 228578dfb3..cd6769afc9 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt @@ -842,4 +842,4 @@ open class JavaMethodTestRunner : TestRunner, KClass<*>?, J private val KFunction<*>.declaringClass: Class<*>? get() = (javaMethod ?: javaConstructor)?.declaringClass -private typealias StaticsType = Map> \ No newline at end of file +private typealias StaticsType = Map> diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt index dd7e3717d4..2aa5de47a7 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt @@ -17,6 +17,7 @@ import org.usvm.util.isException import kotlin.math.pow internal class RecursionTest : ApproximationsTestRunner() { + @UsvmTest([Options([PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM])]) fun testFactorial(options: UMachineOptions) { withOptions(options) { @@ -81,12 +82,15 @@ internal class RecursionTest : ApproximationsTestRunner() { @Test fun vertexSumTest() { - checkDiscoveredProperties( - Recursion::vertexSum, - between(2..3), - { _, x, _ -> x <= 10 }, - { _, x, _ -> x > 10 } - ) + val options = options.copy(stepsFromLastCovered = 4500L) + withOptions(options) { + checkDiscoveredProperties( + Recursion::vertexSum, + between(2..3), + { _, x, _ -> x <= 10 }, + { _, x, _ -> x > 10 } + ) + } } @Test