Merge pull request #961 from GaloisInc/testResolved

Modify `testResolved` to detect partially-overlapping points-tos.
GaloisInc · Jan 22, 2021 · f87988f · f87988f
2 parents 89c562b + d2803c8
commit f87988f
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git a/intTests/test_jvm_setup_errors/test.saw b/intTests/test_jvm_setup_errors/test.saw
@@ -345,7 +345,7 @@ check_fails test "lookup"
   };
 
 print "jvm_array_is with previous jvm_elem_is";
-KNOWN_FALSE_POSITIVE test "lookup"
+check_fails test "lookup"
   do {
     arr <- jvm_alloc_array 8 java_long;
     xs <- jvm_fresh_var "xs" (java_array 8 java_long);

diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs
@@ -24,7 +24,6 @@ Grow\", and is prevalent across the Crucible codebase.
 module SAWScript.Crucible.Common.MethodSpec where
 
 import           Data.Constraint (Constraint)
-import           Data.List (isPrefixOf)
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Void (Void)
@@ -286,8 +285,11 @@ testResolved val0 path0 rs = go path0 val0
         _                  -> False
 
     test _ Nothing = False
-    test path (Just paths) = any (`isPrefixOf` path) paths
+    test path (Just paths) = any (overlap path) paths
 
+    overlap (x : xs) (y : ys) = x == y && overlap xs ys
+    overlap [] _ = True
+    overlap _ [] = True
 
 --------------------------------------------------------------------------------
 -- *** Extension-specific information