Fix not adding initial methods to coverage zone

PySymGym · Jul 7, 2024 · 042b6ea · 042b6ea
1 parent b560b01
commit 042b6ea
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt
@@ -183,8 +183,14 @@ fun <Method, Statement, State, Block> createAIPathSelector(
         addOnCoveredObserver { _, _, statement ->
             blockGraph.blockOf(statement).coveredByTest = true
         }
+        fun addBlocksToCoverageZone(method: Method) {
+            val blocksOfMethod = blockGraph.blocks.filter { blockGraph.methodOf(it) == method }
+            blocksOfMethod.forEach { it.inCoverageZone = true }
+        }
+        // initial methods
+        coverageZone.forEach(::addBlocksToCoverageZone)
         addOnMethodAddedObserver { method ->
-            blockGraph.blocks.filter { blockGraph.methodOf(it) == method }.forEach { it.inCoverageZone = true }
+            addBlocksToCoverageZone(method)
         }
     }
 

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt
@@ -63,6 +63,7 @@ class JcMachine(
         val initialStates = mutableMapOf<JcMethod, JcState>()
         methods.forEach {
             initialStates[it] = interpreter.getInitialState(it, targets)
+            blockGraph.addNewMethod(it)
         }
 
         val methodsToTrackCoverage =