Fix error in that does not correctly handle non-zero offset arrays.

GaloisInc · Mar 16, 2022 · 308e87f · 308e87f
1 parent 87ab2f3
commit 308e87f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -4575,7 +4575,7 @@ permForLLVMArrayBorrow ap (FieldBorrow cell) =
   ValPerm_LLVMBlock $ llvmArrayCellPerm ap cell
 permForLLVMArrayBorrow ap (RangeBorrow (BVRange off len)) =
   ValPerm_Conj1 $ Perm_LLVMArray $
-  ap { llvmArrayOffset = llvmArrayCellToOffset ap off,
+  ap { llvmArrayOffset = llvmArrayCellToAbsOffset ap off,
        llvmArrayLen = len,
        llvmArrayBorrows = [] }