Skip to content

Commit a94512a

Browse files
author
Brian Huffman
committed
Modify testResolved to detect partially-overlapping points-tos.
Previously `testResolved` would detect a later points-to that pointed entirely inside the region of an earlier points-to, but would not detect an overlap if the points-tos were done in the opposite order. This change makes the points-to comparison symmetric, so overlapping points-to declarations are detected no matter what order they appear in a spec. This fixes one of the remaining known false positives from #938.
1 parent 0748c96 commit a94512a

File tree

2 files changed

+5
-3
lines changed

2 files changed

+5
-3
lines changed

intTests/test_jvm_setup_errors/test.saw

+1-1
Original file line numberDiff line numberDiff line change
@@ -345,7 +345,7 @@ check_fails test "lookup"
345345
};
346346

347347
print "jvm_array_is with previous jvm_elem_is";
348-
KNOWN_FALSE_POSITIVE test "lookup"
348+
check_fails test "lookup"
349349
do {
350350
arr <- jvm_alloc_array 8 java_long;
351351
xs <- jvm_fresh_var "xs" (java_array 8 java_long);

src/SAWScript/Crucible/Common/MethodSpec.hs

+4-2
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@ Grow\", and is prevalent across the Crucible codebase.
2424
module SAWScript.Crucible.Common.MethodSpec where
2525

2626
import Data.Constraint (Constraint)
27-
import Data.List (isPrefixOf)
2827
import Data.Map (Map)
2928
import qualified Data.Map as Map
3029
import Data.Void (Void)
@@ -286,8 +285,11 @@ testResolved val0 path0 rs = go path0 val0
286285
_ -> False
287286

288287
test _ Nothing = False
289-
test path (Just paths) = any (`isPrefixOf` path) paths
288+
test path (Just paths) = any (overlap path) paths
290289

290+
overlap (x : xs) (y : ys) = x == y && overlap xs ys
291+
overlap [] _ = True
292+
overlap _ [] = True
291293

292294
--------------------------------------------------------------------------------
293295
-- *** Extension-specific information

0 commit comments

Comments
 (0)