Fix bug that prevented detection of two jvm_field_is on same field.

Fixes #937.
GaloisInc · Dec 4, 2020 · 0a301aa · 0a301aa
1 parent e902b54
commit 0a301aa
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/intTests/test_jvm_setup_errors/test.saw b/intTests/test_jvm_setup_errors/test.saw
@@ -110,7 +110,7 @@ check_fails test "get"
   };
 
 print "jvm_field_is with previous jvm_field_is on same field";
-KNOWN_FALSE_POSITIVE test "get"
+check_fails test "get"
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;

diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
@@ -920,7 +920,7 @@ jvm_field_is ptr fname val =
      let cc = st ^. Setup.csCrucibleContext
      let cb = cc ^. jccCodebase
      let path = Left fname
-     if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [] rs
+     if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [path] rs
        then X.throwM $ JVMFieldMultiple ptr fname
        else Setup.csResolvedState %= MS.markResolved ptr [path]
      let env = MS.csAllocations (st ^. Setup.csMethodSpec)